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

Theorem rexbidv 2327
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 𝑥𝜑
2 ralbidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2rexbid 2325 1 (𝜑 → (∃𝑥𝐴 𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wrex 2307
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 2312
This theorem is referenced by:  rexbii  2331  2rexbidv  2349  rexralbidv  2350  rexeqbi1dv  2514  rexeqbidv  2518  cbvrex2v  2542  rspc2ev  2664  rspc3ev  2666  ceqsrex2v  2676  sbcrext  2835  uniiunlem  3028  eliun  3661  dfiin2g  3690  dfiunv2  3693  nn0suc  4327  rexxpf  4483  elrnmpt  4583  elrnmptg  4586  elimag  4672  funcnvuni  4968  fun11iun  5147  fvelrnb  5221  fvelimab  5229  foelrn  5317  foco2  5318  elabrex  5397  abrexco  5398  f1oiso  5465  f1oiso2  5466  acexmidlemab  5506  acexmidlemcase  5507  grprinvlem  5695  abrexex2g  5747  abrexex2  5751  recseq  5921  tfr0  5937  freceq1  5979  frec0g  5983  frecsuclem3  5990  frecsuc  5991  nnaordex  6100  qseq2  6155  elqsg  6156  isfi  6241  enfi  6334  ltexnqq  6504  elinp  6570  prnmaxl  6584  prnminu  6585  prarloclem3  6593  ltdfpr  6602  genpdflem  6603  genipv  6605  genpassl  6620  genpassu  6621  ltexprlemm  6696  ltexprlemloc  6703  cauappcvgprlemm  6741  cauappcvgprlemopl  6742  cauappcvgprlemlol  6743  cauappcvgprlemopu  6744  cauappcvgprlemupu  6745  cauappcvgprlemdisj  6747  cauappcvgprlemloc  6748  cauappcvgprlemladdfu  6750  cauappcvgprlemladdfl  6751  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  cauappcvgprlem1  6755  cauappcvgprlem2  6756  caucvgprlemm  6764  caucvgprlemopl  6765  caucvgprlemlol  6766  caucvgprlemopu  6767  caucvgprlemupu  6768  caucvgprlemdisj  6770  caucvgprlemloc  6771  caucvgprlemladdfu  6773  caucvgprlemladdrl  6774  caucvgprlem1  6775  caucvgprlem2  6776  caucvgprprlemell  6781  caucvgprprlemelu  6782  caucvgprprlemml  6790  caucvgprprlemmu  6791  caucvgprprlemexbt  6802  caucvgprprlem2  6806  recexgt0sr  6856  archsr  6864  axprecex  6952  nntopi  6966  cnegex  7187  apreap  7576  recexap  7632  creur  7909  creui  7910  cju  7911  qbtwnzlemshrink  9102  rebtwn2zlemshrink  9106  shftfvalg  9417  shftfval  9420  recvguniq  9591  clim  9800  sumeq1  9872  bj-inf2vnlem1  10093  bj-inf2vnlem2  10094  bj-nn0sucALT  10101
  Copyright terms: Public domain W3C validator