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

Theorem rexbidv 2344
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
ralbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
rexbidv  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem rexbidv
StepHypRef Expression
1 nfv 1437 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2rexbid 2342 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102   E.wrex 2324
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-rex 2329
This theorem is referenced by:  rexbii  2348  2rexbidv  2366  rexralbidv  2367  rexeqbi1dv  2531  rexeqbidv  2535  cbvrex2v  2559  rspc2ev  2686  rspc3ev  2688  ceqsrex2v  2698  sbcrext  2862  uniiunlem  3055  eliun  3688  dfiin2g  3717  dfiunv2  3720  nn0suc  4354  rexxpf  4510  elrnmpt  4610  elrnmptg  4613  elimag  4699  funcnvuni  4995  fun11iun  5174  fvelrnb  5248  fvelimab  5256  foelrn  5344  foco2  5345  elabrex  5424  abrexco  5425  f1oiso  5492  f1oiso2  5493  acexmidlemab  5533  acexmidlemcase  5534  grprinvlem  5722  abrexex2g  5774  abrexex2  5778  recseq  5951  tfr0  5967  freceq1  6009  frec0g  6013  frecsuclem3  6020  frecsuc  6021  nnaordex  6130  qseq2  6185  elqsg  6186  isfi  6271  enfi  6364  supeq3  6395  supmoti  6398  suplubti  6405  supisolem  6411  ltexnqq  6563  elinp  6629  prnmaxl  6643  prnminu  6644  prarloclem3  6652  ltdfpr  6661  genpdflem  6662  genipv  6664  genpassl  6679  genpassu  6680  ltexprlemm  6755  ltexprlemloc  6762  cauappcvgprlemm  6800  cauappcvgprlemopl  6801  cauappcvgprlemlol  6802  cauappcvgprlemopu  6803  cauappcvgprlemupu  6804  cauappcvgprlemdisj  6806  cauappcvgprlemloc  6807  cauappcvgprlemladdfu  6809  cauappcvgprlemladdfl  6810  cauappcvgprlemladdru  6811  cauappcvgprlemladdrl  6812  cauappcvgprlem1  6814  cauappcvgprlem2  6815  caucvgprlemm  6823  caucvgprlemopl  6824  caucvgprlemlol  6825  caucvgprlemopu  6826  caucvgprlemupu  6827  caucvgprlemdisj  6829  caucvgprlemloc  6830  caucvgprlemladdfu  6832  caucvgprlemladdrl  6833  caucvgprlem1  6834  caucvgprlem2  6835  caucvgprprlemell  6840  caucvgprprlemelu  6841  caucvgprprlemml  6849  caucvgprprlemmu  6850  caucvgprprlemexbt  6861  caucvgprprlem2  6865  recexgt0sr  6915  archsr  6923  axprecex  7011  nntopi  7025  cnegex  7251  apreap  7651  recexap  7707  creur  7986  creui  7987  cju  7988  qbtwnzlemshrink  9205  rebtwn2zlemshrink  9209  modqmuladd  9315  shftfvalg  9646  shftfval  9649  rexfiuz  9815  recvguniq  9821  clim  10032  sumeq1  10104  divides  10109  odd2np1lem  10182  opeo  10208  omeo  10209  bj-inf2vnlem1  10461  bj-inf2vnlem2  10462  bj-nn0sucALT  10469
  Copyright terms: Public domain W3C validator