Theorem rexbidv 2471

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 1521	. 2 |- F/ x ph
2		ralbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	rexbid 2469	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

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

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-rex 2454

This theorem is referenced by:  rexbii  2477  2rexbidv  2495  rexralbidv  2496  rexeqbi1dv  2674  rexeqbidv  2678  cbvrex2vw  2708  cbvrex2v  2710  rspc2ev  2849  rspc3ev  2851  ceqsrex2v  2862  sbcrext  3032  uniiunlem  3236  eliun  3877  dfiin2g  3906  dfiunv2  3909  nn0suc  4588  rexxpf  4758  elrnmpt  4860  elrnmptg  4863  elimag  4957  funcnvuni  5267  fun11iun  5463  fvelrnb  5544  fvelimab  5552  foco2  5733  elabrex  5737  abrexco  5738  f1oiso  5805  f1oiso2  5806  acexmidlemab  5847  acexmidlemcase  5848  abrexex2g  6099  abrexex2  6103  recseq  6285  tfr0dm  6301  tfr1onlemaccex  6327  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllemaccex  6340  tfrcllemres  6341  freceq1  6371  frec0g  6376  freccllem  6381  frecfcllem  6383  frecsuclem  6385  frecsuc  6386  nnaordex  6507  qseq2  6562  elqsg  6563  elixpsn  6713  ixpsnf1o  6714  isfi  6739  enfi  6851  fimax2gtri  6879  elfi  6948  supeq3  6967  supmoti  6970  suplubti  6977  supisolem  6985  cnvinfex  6995  eqinfti  6997  infvalti  6999  infglbti  7002  enomnilem  7114  finomni  7116  exmidomni  7118  fodjum  7122  fodju0  7123  fodjuomnilemres  7124  fodjuomni  7125  ismkvnex  7131  fodjumkvlemres  7135  fodjumkv  7136  enmkvlem  7137  ltexnqq  7370  elinp  7436  prnmaxl  7450  prnminu  7451  prarloclem3  7459  ltdfpr  7468  genpdflem  7469  genipv  7471  genpassl  7486  genpassu  7487  ltexprlemm  7562  ltexprlemloc  7569  cauappcvgprlemm  7607  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemopu  7610  cauappcvgprlemupu  7611  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  cauappcvgprlem2  7622  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemopu  7633  caucvgprlemupu  7634  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprlem1  7641  caucvgprlem2  7642  caucvgprprlemell  7647  caucvgprprlemelu  7648  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemexbt  7668  caucvgprprlem2  7672  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemub  7685  recexgt0sr  7735  archsr  7744  map2psrprg  7767  suplocsrlemb  7768  axprecex  7842  nntopi  7856  axpre-suploclemres  7863  axpre-suploc  7864  cnegex  8097  apreap  8506  recexap  8571  sup3exmid  8873  creur  8875  creui  8876  cju  8877  supinfneg  9554  infsupneg  9555  exbtwnzlemshrink  10205  rebtwn2zlemshrink  10210  modqmuladd  10322  hashunlem  10739  shftfvalg  10782  shftfval  10785  rexfiuz  10953  recvguniq  10959  fimaxre2  11190  clim  11244  sumeq1  11318  summodc  11346  fsum3  11350  mertenslemub  11497  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  prodeq1f  11515  prodeq2w  11519  prodmodc  11541  fprodseq  11546  divides  11751  odd2np1lem  11831  opeo  11856  omeo  11857  divalglemeunn  11880  divalglemeuneg  11882  infssuzex  11904  nninfdcex  11908  zeqzmulgcd  11925  bezoutlemnewy  11951  bezoutlemmain  11953  bezoutlemex  11956  bezoutlemaz  11958  exprmfct  12092  nnnn0modprm0  12209  pceu  12249  pcprmpw2  12286  ennnfoneleminc  12366  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemnn0  12377  ennnfonelemr  12378  ctinfomlemom  12382  ctinfom  12383  nninfdclemcl  12403  nninfdclemp1  12405  nninfdc  12408  grprinvlem  12639  isnsgrp  12647  grpinvex  12718  dfgrp2  12732  grpidinv2  12758  grpidinv  12759  basis2  12840  eltg2  12847  tg2  12854  neival  12937  isnei  12938  isneip  12940  restbasg  12962  cnpval  12992  iscnp  12993  icnpimaex  13005  lmbr  13007  lmbr2  13008  cnptoprest2  13034  lmff  13043  txbas  13052  txcnp  13065  txrest  13070  blssps  13221  blss  13222  mopni  13276  metss  13288  metrest  13300  metcnp3  13305  divcnap  13349  cncfval  13353  elcncf2  13355  cncfmet  13373  dedekindeulemuub  13389  dedekindeulemloc  13391  dedekindeulemlu  13393  suplociccreex  13396  dedekindicclemuub  13398  dedekindicclemloc  13400  dedekindicclemlu  13402  limccl  13422  ellimc3apf  13423  limcdifap  13425  limcmpted  13426  bj-inf2vnlem1  14005  bj-inf2vnlem2  14006  bj-nn0sucALT  14013  sscoll2  14023  subctctexmid  14034  pw1nct  14036  isomninnlem  14062  trilpolemlt1  14073  trirec0  14076  ismkvnnlem  14084