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

Theorem rexbidv 2377
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 1464 . 2  |-  F/ x ph
2 ralbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2rexbid 2375 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 2356
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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-rex 2361
This theorem is referenced by:  rexbii  2381  2rexbidv  2399  rexralbidv  2400  rexeqbi1dv  2567  rexeqbidv  2571  cbvrex2v  2595  rspc2ev  2728  rspc3ev  2730  ceqsrex2v  2740  sbcrext  2905  uniiunlem  3098  eliun  3717  dfiin2g  3746  dfiunv2  3749  nn0suc  4392  rexxpf  4551  elrnmpt  4652  elrnmptg  4655  elimag  4745  funcnvuni  5048  fun11iun  5237  fvelrnb  5315  fvelimab  5323  foelrnOLD  5493  foco2  5494  elabrex  5498  abrexco  5499  f1oiso  5566  f1oiso2  5567  acexmidlemab  5607  acexmidlemcase  5608  grprinvlem  5796  abrexex2g  5848  abrexex2  5852  recseq  6025  tfr0dm  6041  tfr1onlemaccex  6067  tfrcllemsucaccv  6073  tfrcllembxssdm  6075  tfrcllemaccex  6080  tfrcllemres  6081  freceq1  6111  frec0g  6116  freccllem  6121  frecfcllem  6123  frecsuclem  6125  frecsuc  6126  nnaordex  6238  qseq2  6293  elqsg  6294  isfi  6430  enfi  6541  fimax2gtri  6569  supeq3  6629  supmoti  6632  suplubti  6639  supisolem  6647  cnvinfex  6657  eqinfti  6659  infvalti  6661  infglbti  6664  enomnilem  6738  finomni  6740  exmidomni  6742  fodjuomnilemm  6745  fodjuomnilem0  6746  fodjuomnilemres  6747  fodjuomni  6748  ltexnqq  6911  elinp  6977  prnmaxl  6991  prnminu  6992  prarloclem3  7000  ltdfpr  7009  genpdflem  7010  genipv  7012  genpassl  7027  genpassu  7028  ltexprlemm  7103  ltexprlemloc  7110  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemlol  7150  cauappcvgprlemopu  7151  cauappcvgprlemupu  7152  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  cauappcvgprlem1  7162  cauappcvgprlem2  7163  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemopu  7174  caucvgprlemupu  7175  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprlem1  7182  caucvgprlem2  7183  caucvgprprlemell  7188  caucvgprprlemelu  7189  caucvgprprlemml  7197  caucvgprprlemmu  7198  caucvgprprlemexbt  7209  caucvgprprlem2  7213  recexgt0sr  7263  archsr  7271  axprecex  7359  nntopi  7373  cnegex  7604  apreap  8005  recexap  8061  creur  8354  creui  8355  cju  8356  supinfneg  9015  infsupneg  9016  exbtwnzlemshrink  9588  rebtwn2zlemshrink  9593  modqmuladd  9701  hashunlem  10108  shftfvalg  10148  shftfval  10151  rexfiuz  10317  recvguniq  10323  fimaxre2  10551  clim  10562  sumeq1  10634  isummo  10662  fisum  10665  divides  10673  odd2np1lem  10747  opeo  10772  omeo  10773  divalglemeunn  10796  divalglemeuneg  10798  infssuzex  10820  zeqzmulgcd  10837  bezoutlemnewy  10860  bezoutlemmain  10862  bezoutlemex  10865  bezoutlemaz  10867  exprmfct  10994  bj-inf2vnlem1  11303  bj-inf2vnlem2  11304  bj-nn0sucALT  11311
  Copyright terms: Public domain W3C validator