ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rexbidv Unicode version

Theorem rexbidv 2324
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
ralbidv.1
Assertion
Ref Expression
rexbidv
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem rexbidv
StepHypRef Expression
1 nfv 1421 . 2  F/
2 ralbidv.1 . 2
31, 2rexbid 2322 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98  wrex 2304
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-rex 2309
This theorem is referenced by:  rexbii  2328  2rexbidv  2346  rexralbidv  2347  rexeqbi1dv  2511  rexeqbidv  2515  cbvrex2v  2539  rspc2ev  2661  rspc3ev  2663  ceqsrex2v  2673  sbcrext  2832  sbcrexg  2834  uniiunlem  3025  eliun  3655  dfiin2g  3684  dfiunv2  3687  nn0suc  4273  rexxpf  4429  elrnmpt  4529  elrnmptg  4532  elimag  4618  funcnvuni  4914  fun11iun  5093  fvelrnb  5167  fvelimab  5175  foelrn  5263  foco2  5264  elabrex  5343  abrexco  5344  f1oiso  5411  f1oiso2  5412  acexmidlemab  5452  acexmidlemcase  5453  grprinvlem  5640  abrexex2g  5692  abrexex2  5696  recseq  5866  tfr0  5882  freceq1  5923  frec0g  5926  frecsuclem3  5933  frecsuc  5934  nnaordex  6040  qseq2  6095  elqsg  6096  isfi  6181  enfi  6256  ltexnqq  6396  elinp  6462  prnmaxl  6476  prnminu  6477  prarloclem3  6485  ltdfpr  6494  genpdflem  6495  genipv  6497  genpassl  6512  genpassu  6513  ltexprlemm  6588  ltexprlemloc  6595  cauappcvgprlemm  6633  cauappcvgprlemopl  6634  cauappcvgprlemlol  6635  cauappcvgprlemopu  6636  cauappcvgprlemupu  6637  cauappcvgprlemdisj  6639  cauappcvgprlemloc  6640  cauappcvgprlemladdfu  6642  cauappcvgprlemladdfl  6643  cauappcvgprlemladdru  6644  cauappcvgprlemladdrl  6645  cauappcvgprlem1  6647  cauappcvgprlem2  6648  caucvgprlemm  6656  caucvgprlemopl  6657  caucvgprlemlol  6658  caucvgprlemopu  6659  caucvgprlemupu  6660  caucvgprlemdisj  6662  caucvgprlemloc  6663  caucvgprlemladdfu  6665  caucvgprlemladdrl  6666  caucvgprlem1  6667  caucvgprlem2  6668  caucvgprprlemell  6673  caucvgprprlemelu  6674  caucvgprprlemml  6682  caucvgprprlemmu  6683  caucvgprprlemexbt  6694  caucvgprprlem2  6698  recexgt0sr  6748  archsr  6756  axprecex  6844  nntopi  6858  cnegex  7078  apreap  7463  recexap  7508  creur  7784  creui  7785  cju  7786  bj-inf2vnlem1  9538  bj-inf2vnlem2  9539  bj-nn0sucALT  9546
  Copyright terms: Public domain W3C validator