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

Theorem rexbidv 2375
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 1462 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2rexbid 2373 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   E.wrex 2354
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-rex 2359
This theorem is referenced by:  rexbii  2379  2rexbidv  2397  rexralbidv  2398  rexeqbi1dv  2564  rexeqbidv  2568  cbvrex2v  2592  rspc2ev  2725  rspc3ev  2727  ceqsrex2v  2737  sbcrext  2902  uniiunlem  3093  eliun  3708  dfiin2g  3737  dfiunv2  3740  nn0suc  4381  rexxpf  4539  elrnmpt  4640  elrnmptg  4643  elimag  4731  funcnvuni  5034  fun11iun  5220  fvelrnb  5295  fvelimab  5303  foelrnOLD  5470  foco2  5471  elabrex  5475  abrexco  5476  f1oiso  5542  f1oiso2  5543  acexmidlemab  5583  acexmidlemcase  5584  grprinvlem  5772  abrexex2g  5824  abrexex2  5828  recseq  6001  tfr0dm  6017  tfr1onlemaccex  6043  tfrcllemsucaccv  6049  tfrcllembxssdm  6051  tfrcllemaccex  6056  tfrcllemres  6057  freceq1  6087  frec0g  6092  freccllem  6097  frecfcllem  6099  frecsuclem  6101  frecsuc  6102  nnaordex  6214  qseq2  6269  elqsg  6270  isfi  6406  enfi  6517  supeq3  6590  supmoti  6593  suplubti  6600  supisolem  6608  cnvinfex  6618  eqinfti  6620  infvalti  6622  infglbti  6625  enomnilem  6697  finomni  6699  exmidomni  6701  fodjuomnilemm  6704  fodjuomnilem0  6705  fodjuomnilemres  6706  fodjuomni  6707  ltexnqq  6868  elinp  6934  prnmaxl  6948  prnminu  6949  prarloclem3  6957  ltdfpr  6966  genpdflem  6967  genipv  6969  genpassl  6984  genpassu  6985  ltexprlemm  7060  ltexprlemloc  7067  cauappcvgprlemm  7105  cauappcvgprlemopl  7106  cauappcvgprlemlol  7107  cauappcvgprlemopu  7108  cauappcvgprlemupu  7109  cauappcvgprlemdisj  7111  cauappcvgprlemloc  7112  cauappcvgprlemladdfu  7114  cauappcvgprlemladdfl  7115  cauappcvgprlemladdru  7116  cauappcvgprlemladdrl  7117  cauappcvgprlem1  7119  cauappcvgprlem2  7120  caucvgprlemm  7128  caucvgprlemopl  7129  caucvgprlemlol  7130  caucvgprlemopu  7131  caucvgprlemupu  7132  caucvgprlemdisj  7134  caucvgprlemloc  7135  caucvgprlemladdfu  7137  caucvgprlemladdrl  7138  caucvgprlem1  7139  caucvgprlem2  7140  caucvgprprlemell  7145  caucvgprprlemelu  7146  caucvgprprlemml  7154  caucvgprprlemmu  7155  caucvgprprlemexbt  7166  caucvgprprlem2  7170  recexgt0sr  7220  archsr  7228  axprecex  7316  nntopi  7330  cnegex  7561  apreap  7962  recexap  8018  creur  8311  creui  8312  cju  8313  supinfneg  8976  infsupneg  8977  exbtwnzlemshrink  9547  rebtwn2zlemshrink  9552  modqmuladd  9660  hashunlem  10045  shftfvalg  10078  shftfval  10081  rexfiuz  10247  recvguniq  10253  fimaxre2  10481  clim  10492  sumeq1  10564  divides  10576  odd2np1lem  10650  opeo  10675  omeo  10676  divalglemeunn  10699  divalglemeuneg  10701  infssuzex  10723  zeqzmulgcd  10740  bezoutlemnewy  10763  bezoutlemmain  10765  bezoutlemex  10768  bezoutlemaz  10770  exprmfct  10897  bj-inf2vnlem1  11206  bj-inf2vnlem2  11207  bj-nn0sucALT  11214
  Copyright terms: Public domain W3C validator