Theorem rexbidv 2545

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

Syntax hints:   -> wi 4   <-> wb 105   E.wrex 2523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-rex 2528

This theorem is referenced by:  rexbii  2551  2rexbidv  2569  rexralbidv  2570  rexeqbi1dv  2756  rexeqbidv  2760  cbvrex2vw  2792  cbvrex2v  2794  rspc2ev  2938  rspc3ev  2940  ceqsrex2v  2951  sbcrext  3122  uniiunlem  3330  eliun  3997  dfiin2g  4026  dfiunv2  4029  nn0suc  4728  rexxpf  4904  elrnmpt  5008  elrnmptg  5011  elimag  5107  funcnvuni  5427  fun11iun  5637  fvelrnb  5726  fvelimab  5735  foco2  5928  elabrex  5932  elabrexg  5933  abrexco  5934  f1oiso  6001  f1oiso2  6002  acexmidlemab  6046  acexmidlemcase  6047  abrexex2g  6315  abrexex2  6319  recseq  6539  tfr0dm  6555  tfr1onlemaccex  6581  tfrcllemsucaccv  6587  tfrcllembxssdm  6589  tfrcllemaccex  6594  tfrcllemres  6595  freceq1  6625  frec0g  6630  freccllem  6635  frecfcllem  6637  frecsuclem  6639  frecsuc  6640  nnaordex  6763  qseq2  6820  elqsg  6821  elixpsn  6972  ixpsnf1o  6973  isfi  7002  enfi  7130  fimax2gtri  7161  elfi  7260  supeq3  7283  supmoti  7286  suplubti  7293  supisolem  7301  cnvinfex  7311  eqinfti  7313  infvalti  7315  infglbti  7318  enomnilem  7431  finomni  7433  exmidomni  7435  fodjum  7439  fodju0  7440  fodjuomnilemres  7441  fodjuomni  7442  ismkvnex  7448  fodjumkvlemres  7452  fodjumkv  7453  enmkvlem  7454  ltexnqq  7725  elinp  7791  prnmaxl  7805  prnminu  7806  prarloclem3  7814  ltdfpr  7823  genpdflem  7824  genipv  7826  genpassl  7841  genpassu  7842  ltexprlemm  7917  ltexprlemloc  7924  cauappcvgprlemm  7962  cauappcvgprlemopl  7963  cauappcvgprlemlol  7964  cauappcvgprlemopu  7965  cauappcvgprlemupu  7966  cauappcvgprlemdisj  7968  cauappcvgprlemloc  7969  cauappcvgprlemladdfu  7971  cauappcvgprlemladdfl  7972  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  cauappcvgprlem1  7976  cauappcvgprlem2  7977  caucvgprlemm  7985  caucvgprlemopl  7986  caucvgprlemlol  7987  caucvgprlemopu  7988  caucvgprlemupu  7989  caucvgprlemdisj  7991  caucvgprlemloc  7992  caucvgprlemladdfu  7994  caucvgprlemladdrl  7995  caucvgprlem1  7996  caucvgprlem2  7997  caucvgprprlemell  8002  caucvgprprlemelu  8003  caucvgprprlemml  8011  caucvgprprlemmu  8012  caucvgprprlemexbt  8023  caucvgprprlem2  8027  suplocexprlemmu  8035  suplocexprlemru  8036  suplocexprlemdisj  8037  suplocexprlemloc  8038  suplocexprlemub  8040  recexgt0sr  8090  archsr  8099  map2psrprg  8122  suplocsrlemb  8123  axprecex  8197  nntopi  8211  axpre-suploclemres  8218  axpre-suploc  8219  cnegex  8453  apreap  8863  recexap  8929  sup3exmid  9233  creur  9235  creui  9236  cju  9237  supinfneg  9930  infsupneg  9931  infssuzex  10597  nninfdcex  10601  exbtwnzlemshrink  10612  rebtwn2zlemshrink  10617  modqmuladd  10732  hashunlem  11172  iswrd  11230  csbwrdg  11258  shftfvalg  11507  shftfval  11510  rexfiuz  11678  recvguniq  11684  fimaxre2  11916  clim  11970  sumeq1  12044  summodc  12073  fsum3  12077  mertenslemub  12224  mertenslemi1  12225  mertenslem2  12226  mertensabs  12227  prodeq1f  12242  prodeq2w  12246  prodmodc  12268  fprodseq  12273  divides  12479  odd2np1lem  12562  opeo  12587  omeo  12588  divalglemeunn  12611  divalglemeuneg  12613  zeqzmulgcd  12670  bezoutlemnewy  12696  bezoutlemmain  12698  bezoutlemex  12701  bezoutlemaz  12703  exprmfct  12839  nnnn0modprm0  12957  pceu  12997  pcprmpw2  13035  4sqlemafi  13097  4sqexercise1  13100  4sqlem12  13104  ennnfoneleminc  13179  ennnfonelemex  13182  ennnfonelemhom  13183  ennnfonelemnn0  13190  ennnfonelemr  13191  ctinfomlemom  13195  ctinfom  13196  nninfdclemcl  13216  nninfdclemp1  13218  nninfdc  13221  ptex  13494  grpinvalem  13615  igsumvalx  13619  gsumpropd  13622  gsumress  13625  gsum0g  13626  isnsgrp  13636  grpinvex  13740  dfgrp2  13757  grpidinv2  13788  grpidinv  13789  dfgrp3mlem  13828  grp1  13836  imasgrp2  13844  dvdsrd  14256  opprunitd  14272  subrgdvds  14397  lss1d  14548  lspsn  14581  ellspsn  14582  rspsn  14699  znf1o  14816  basis2  14930  eltg2  14935  tg2  14942  neival  15025  isnei  15026  isneip  15028  restbasg  15050  cnpval  15080  iscnp  15081  icnpimaex  15093  lmbr  15095  lmbr2  15096  cnptoprest2  15122  lmff  15131  txbas  15140  txcnp  15153  txrest  15158  blssps  15309  blss  15310  mopni  15364  metss  15376  metrest  15388  metcnp3  15393  divcnap  15447  cncfval  15454  elcncf2  15456  cncfmet  15474  dedekindeulemuub  15499  dedekindeulemloc  15501  dedekindeulemlu  15503  suplociccreex  15506  dedekindicclemuub  15508  dedekindicclemloc  15510  dedekindicclemlu  15512  ivthreinc  15527  limccl  15541  ellimc3apf  15542  limcdifap  15544  limcmpted  15545  plyval  15614  elply2  15617  2lgslem1b  15979  upgredg2vtx  16160  usgredg4  16227  ushgredgedg  16238  ushgredgedgloop  16240  vtxd0nedgbfi  16311  bj-inf2vnlem1  16757  bj-inf2vnlem2  16758  bj-nn0sucALT  16765  sscoll2  16775  3dom  16779  subctctexmid  16791  pw1nct  16794  isomninnlem  16831  trilpolemlt1  16842  trirec0  16845  qdiff  16850  ismkvnnlem  16854