Theorem rexbidv 2467

Description: Formula-building rule for restricted existential quantifier (deduction form). (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

Step	Hyp	Ref	Expression
1		nfv 1516	. 2 |- F/ x ph
2		ralbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	rexbid 2465	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Syntax hints:   -> wi 4   <-> wb 104   E.wrex 2445

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-rex 2450

This theorem is referenced by:  rexbii  2473  2rexbidv  2491  rexralbidv  2492  rexeqbi1dv  2670  rexeqbidv  2674  cbvrex2vw  2704  cbvrex2v  2706  rspc2ev  2845  rspc3ev  2847  ceqsrex2v  2858  sbcrext  3028  uniiunlem  3231  eliun  3870  dfiin2g  3899  dfiunv2  3902  nn0suc  4581  rexxpf  4751  elrnmpt  4853  elrnmptg  4856  elimag  4950  funcnvuni  5257  fun11iun  5453  fvelrnb  5534  fvelimab  5542  foco2  5722  elabrex  5726  abrexco  5727  f1oiso  5794  f1oiso2  5795  acexmidlemab  5836  acexmidlemcase  5837  abrexex2g  6088  abrexex2  6092  recseq  6274  tfr0dm  6290  tfr1onlemaccex  6316  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllemaccex  6329  tfrcllemres  6330  freceq1  6360  frec0g  6365  freccllem  6370  frecfcllem  6372  frecsuclem  6374  frecsuc  6375  nnaordex  6495  qseq2  6550  elqsg  6551  elixpsn  6701  ixpsnf1o  6702  isfi  6727  enfi  6839  fimax2gtri  6867  elfi  6936  supeq3  6955  supmoti  6958  suplubti  6965  supisolem  6973  cnvinfex  6983  eqinfti  6985  infvalti  6987  infglbti  6990  enomnilem  7102  finomni  7104  exmidomni  7106  fodjum  7110  fodju0  7111  fodjuomnilemres  7112  fodjuomni  7113  ismkvnex  7119  fodjumkvlemres  7123  fodjumkv  7124  enmkvlem  7125  ltexnqq  7349  elinp  7415  prnmaxl  7429  prnminu  7430  prarloclem3  7438  ltdfpr  7447  genpdflem  7448  genipv  7450  genpassl  7465  genpassu  7466  ltexprlemm  7541  ltexprlemloc  7548  cauappcvgprlemm  7586  cauappcvgprlemopl  7587  cauappcvgprlemlol  7588  cauappcvgprlemopu  7589  cauappcvgprlemupu  7590  cauappcvgprlemdisj  7592  cauappcvgprlemloc  7593  cauappcvgprlemladdfu  7595  cauappcvgprlemladdfl  7596  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  cauappcvgprlem1  7600  cauappcvgprlem2  7601  caucvgprlemm  7609  caucvgprlemopl  7610  caucvgprlemlol  7611  caucvgprlemopu  7612  caucvgprlemupu  7613  caucvgprlemdisj  7615  caucvgprlemloc  7616  caucvgprlemladdfu  7618  caucvgprlemladdrl  7619  caucvgprlem1  7620  caucvgprlem2  7621  caucvgprprlemell  7626  caucvgprprlemelu  7627  caucvgprprlemml  7635  caucvgprprlemmu  7636  caucvgprprlemexbt  7647  caucvgprprlem2  7651  suplocexprlemmu  7659  suplocexprlemru  7660  suplocexprlemdisj  7661  suplocexprlemloc  7662  suplocexprlemub  7664  recexgt0sr  7714  archsr  7723  map2psrprg  7746  suplocsrlemb  7747  axprecex  7821  nntopi  7835  axpre-suploclemres  7842  axpre-suploc  7843  cnegex  8076  apreap  8485  recexap  8550  sup3exmid  8852  creur  8854  creui  8855  cju  8856  supinfneg  9533  infsupneg  9534  exbtwnzlemshrink  10184  rebtwn2zlemshrink  10189  modqmuladd  10301  hashunlem  10717  shftfvalg  10760  shftfval  10763  rexfiuz  10931  recvguniq  10937  fimaxre2  11168  clim  11222  sumeq1  11296  summodc  11324  fsum3  11328  mertenslemub  11475  mertenslemi1  11476  mertenslem2  11477  mertensabs  11478  prodeq1f  11493  prodeq2w  11497  prodmodc  11519  fprodseq  11524  divides  11729  odd2np1lem  11809  opeo  11834  omeo  11835  divalglemeunn  11858  divalglemeuneg  11860  infssuzex  11882  nninfdcex  11886  zeqzmulgcd  11903  bezoutlemnewy  11929  bezoutlemmain  11931  bezoutlemex  11934  bezoutlemaz  11936  exprmfct  12070  nnnn0modprm0  12187  pceu  12227  pcprmpw2  12264  ennnfoneleminc  12344  ennnfonelemex  12347  ennnfonelemhom  12348  ennnfonelemnn0  12355  ennnfonelemr  12356  ctinfomlemom  12360  ctinfom  12361  nninfdclemcl  12381  nninfdclemp1  12383  nninfdc  12386  grprinvlem  12616  basis2  12686  eltg2  12693  tg2  12700  neival  12783  isnei  12784  isneip  12786  restbasg  12808  cnpval  12838  iscnp  12839  icnpimaex  12851  lmbr  12853  lmbr2  12854  cnptoprest2  12880  lmff  12889  txbas  12898  txcnp  12911  txrest  12916  blssps  13067  blss  13068  mopni  13122  metss  13134  metrest  13146  metcnp3  13151  divcnap  13195  cncfval  13199  elcncf2  13201  cncfmet  13219  dedekindeulemuub  13235  dedekindeulemloc  13237  dedekindeulemlu  13239  suplociccreex  13242  dedekindicclemuub  13244  dedekindicclemloc  13246  dedekindicclemlu  13248  limccl  13268  ellimc3apf  13269  limcdifap  13271  limcmpted  13272  bj-inf2vnlem1  13852  bj-inf2vnlem2  13853  bj-nn0sucALT  13860  sscoll2  13870  subctctexmid  13881  pw1nct  13883  isomninnlem  13909  trilpolemlt1  13920  trirec0  13923  ismkvnnlem  13931