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  6506  elinp  6572  prnmaxl  6586  prnminu  6587  prarloclem3  6595  ltdfpr  6604  genpdflem  6605  genipv  6607  genpassl  6622  genpassu  6623  ltexprlemm  6698  ltexprlemloc  6705  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemopu  6746  cauappcvgprlemupu  6747  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  cauappcvgprlem2  6758  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemopu  6769  caucvgprlemupu  6770  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlem1  6777  caucvgprlem2  6778  caucvgprprlemell  6783  caucvgprprlemelu  6784  caucvgprprlemml  6792  caucvgprprlemmu  6793  caucvgprprlemexbt  6804  caucvgprprlem2  6808  recexgt0sr  6858  archsr  6866  axprecex  6954  nntopi  6968  cnegex  7189  apreap  7578  recexap  7634  creur  7911  creui  7912  cju  7913  qbtwnzlemshrink  9104  rebtwn2zlemshrink  9108  shftfvalg  9419  shftfval  9422  recvguniq  9593  clim  9802  sumeq1  9874  bj-inf2vnlem1  10095  bj-inf2vnlem2  10096  bj-nn0sucALT  10103
  Copyright terms: Public domain W3C validator