Theorem rexbidv 2509

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-rex 2492

This theorem is referenced by:  rexbii  2515  2rexbidv  2533  rexralbidv  2534  rexeqbi1dv  2718  rexeqbidv  2722  cbvrex2vw  2754  cbvrex2v  2756  rspc2ev  2899  rspc3ev  2901  ceqsrex2v  2912  sbcrext  3083  uniiunlem  3290  eliun  3945  dfiin2g  3974  dfiunv2  3977  nn0suc  4670  rexxpf  4843  elrnmpt  4946  elrnmptg  4949  elimag  5045  funcnvuni  5362  fun11iun  5565  fvelrnb  5649  fvelimab  5658  foco2  5845  elabrex  5849  elabrexg  5850  abrexco  5851  f1oiso  5918  f1oiso2  5919  acexmidlemab  5961  acexmidlemcase  5962  abrexex2g  6228  abrexex2  6232  recseq  6415  tfr0dm  6431  tfr1onlemaccex  6457  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllemaccex  6470  tfrcllemres  6471  freceq1  6501  frec0g  6506  freccllem  6511  frecfcllem  6513  frecsuclem  6515  frecsuc  6516  nnaordex  6637  qseq2  6694  elqsg  6695  elixpsn  6845  ixpsnf1o  6846  isfi  6875  enfi  6996  fimax2gtri  7024  elfi  7099  supeq3  7118  supmoti  7121  suplubti  7128  supisolem  7136  cnvinfex  7146  eqinfti  7148  infvalti  7150  infglbti  7153  enomnilem  7266  finomni  7268  exmidomni  7270  fodjum  7274  fodju0  7275  fodjuomnilemres  7276  fodjuomni  7277  ismkvnex  7283  fodjumkvlemres  7287  fodjumkv  7288  enmkvlem  7289  ltexnqq  7556  elinp  7622  prnmaxl  7636  prnminu  7637  prarloclem3  7645  ltdfpr  7654  genpdflem  7655  genipv  7657  genpassl  7672  genpassu  7673  ltexprlemm  7748  ltexprlemloc  7755  cauappcvgprlemm  7793  cauappcvgprlemopl  7794  cauappcvgprlemlol  7795  cauappcvgprlemopu  7796  cauappcvgprlemupu  7797  cauappcvgprlemdisj  7799  cauappcvgprlemloc  7800  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem1  7807  cauappcvgprlem2  7808  caucvgprlemm  7816  caucvgprlemopl  7817  caucvgprlemlol  7818  caucvgprlemopu  7819  caucvgprlemupu  7820  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  caucvgprlem1  7827  caucvgprlem2  7828  caucvgprprlemell  7833  caucvgprprlemelu  7834  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemexbt  7854  caucvgprprlem2  7858  suplocexprlemmu  7866  suplocexprlemru  7867  suplocexprlemdisj  7868  suplocexprlemloc  7869  suplocexprlemub  7871  recexgt0sr  7921  archsr  7930  map2psrprg  7953  suplocsrlemb  7954  axprecex  8028  nntopi  8042  axpre-suploclemres  8049  axpre-suploc  8050  cnegex  8285  apreap  8695  recexap  8761  sup3exmid  9065  creur  9067  creui  9068  cju  9069  supinfneg  9751  infsupneg  9752  infssuzex  10413  nninfdcex  10417  exbtwnzlemshrink  10428  rebtwn2zlemshrink  10433  modqmuladd  10548  hashunlem  10986  iswrd  11033  csbwrdg  11060  shftfvalg  11244  shftfval  11247  rexfiuz  11415  recvguniq  11421  fimaxre2  11653  clim  11707  sumeq1  11781  summodc  11809  fsum3  11813  mertenslemub  11960  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  prodeq1f  11978  prodeq2w  11982  prodmodc  12004  fprodseq  12009  divides  12215  odd2np1lem  12298  opeo  12323  omeo  12324  divalglemeunn  12347  divalglemeuneg  12349  zeqzmulgcd  12406  bezoutlemnewy  12432  bezoutlemmain  12434  bezoutlemex  12437  bezoutlemaz  12439  exprmfct  12575  nnnn0modprm0  12693  pceu  12733  pcprmpw2  12771  4sqlemafi  12833  4sqexercise1  12836  4sqlem12  12840  ennnfoneleminc  12897  ennnfonelemex  12900  ennnfonelemhom  12901  ennnfonelemnn0  12908  ennnfonelemr  12909  ctinfomlemom  12913  ctinfom  12914  nninfdclemcl  12934  nninfdclemp1  12936  nninfdc  12939  ptex  13211  grpinvalem  13332  igsumvalx  13336  gsumpropd  13339  gsumress  13342  gsum0g  13343  isnsgrp  13353  grpinvex  13457  dfgrp2  13474  grpidinv2  13505  grpidinv  13506  dfgrp3mlem  13545  grp1  13553  imasgrp2  13561  dvdsrd  13971  opprunitd  13987  subrgdvds  14112  lss1d  14260  lspsn  14293  ellspsn  14294  rspsn  14411  znf1o  14528  basis2  14635  eltg2  14640  tg2  14647  neival  14730  isnei  14731  isneip  14733  restbasg  14755  cnpval  14785  iscnp  14786  icnpimaex  14798  lmbr  14800  lmbr2  14801  cnptoprest2  14827  lmff  14836  txbas  14845  txcnp  14858  txrest  14863  blssps  15014  blss  15015  mopni  15069  metss  15081  metrest  15093  metcnp3  15098  divcnap  15152  cncfval  15159  elcncf2  15161  cncfmet  15179  dedekindeulemuub  15204  dedekindeulemloc  15206  dedekindeulemlu  15208  suplociccreex  15211  dedekindicclemuub  15213  dedekindicclemloc  15215  dedekindicclemlu  15217  ivthreinc  15232  limccl  15246  ellimc3apf  15247  limcdifap  15249  limcmpted  15250  plyval  15319  elply2  15322  2lgslem1b  15681  upgredg2vtx  15852  bj-inf2vnlem1  16105  bj-inf2vnlem2  16106  bj-nn0sucALT  16113  sscoll2  16123  subctctexmid  16139  pw1nct  16142  isomninnlem  16171  trilpolemlt1  16182  trirec0  16185  ismkvnnlem  16193