Theorem rexbidv 2507

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-rex 2490

This theorem is referenced by:  rexbii  2513  2rexbidv  2531  rexralbidv  2532  rexeqbi1dv  2715  rexeqbidv  2719  cbvrex2vw  2750  cbvrex2v  2752  rspc2ev  2892  rspc3ev  2894  ceqsrex2v  2905  sbcrext  3076  uniiunlem  3282  eliun  3931  dfiin2g  3960  dfiunv2  3963  nn0suc  4652  rexxpf  4825  elrnmpt  4927  elrnmptg  4930  elimag  5026  funcnvuni  5343  fun11iun  5543  fvelrnb  5626  fvelimab  5635  foco2  5822  elabrex  5826  elabrexg  5827  abrexco  5828  f1oiso  5895  f1oiso2  5896  acexmidlemab  5938  acexmidlemcase  5939  abrexex2g  6205  abrexex2  6209  recseq  6392  tfr0dm  6408  tfr1onlemaccex  6434  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllemaccex  6447  tfrcllemres  6448  freceq1  6478  frec0g  6483  freccllem  6488  frecfcllem  6490  frecsuclem  6492  frecsuc  6493  nnaordex  6614  qseq2  6671  elqsg  6672  elixpsn  6822  ixpsnf1o  6823  isfi  6852  enfi  6970  fimax2gtri  6998  elfi  7073  supeq3  7092  supmoti  7095  suplubti  7102  supisolem  7110  cnvinfex  7120  eqinfti  7122  infvalti  7124  infglbti  7127  enomnilem  7240  finomni  7242  exmidomni  7244  fodjum  7248  fodju0  7249  fodjuomnilemres  7250  fodjuomni  7251  ismkvnex  7257  fodjumkvlemres  7261  fodjumkv  7262  enmkvlem  7263  ltexnqq  7521  elinp  7587  prnmaxl  7601  prnminu  7602  prarloclem3  7610  ltdfpr  7619  genpdflem  7620  genipv  7622  genpassl  7637  genpassu  7638  ltexprlemm  7713  ltexprlemloc  7720  cauappcvgprlemm  7758  cauappcvgprlemopl  7759  cauappcvgprlemlol  7760  cauappcvgprlemopu  7761  cauappcvgprlemupu  7762  cauappcvgprlemdisj  7764  cauappcvgprlemloc  7765  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlem1  7772  cauappcvgprlem2  7773  caucvgprlemm  7781  caucvgprlemopl  7782  caucvgprlemlol  7783  caucvgprlemopu  7784  caucvgprlemupu  7785  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  caucvgprlem1  7792  caucvgprlem2  7793  caucvgprprlemell  7798  caucvgprprlemelu  7799  caucvgprprlemml  7807  caucvgprprlemmu  7808  caucvgprprlemexbt  7819  caucvgprprlem2  7823  suplocexprlemmu  7831  suplocexprlemru  7832  suplocexprlemdisj  7833  suplocexprlemloc  7834  suplocexprlemub  7836  recexgt0sr  7886  archsr  7895  map2psrprg  7918  suplocsrlemb  7919  axprecex  7993  nntopi  8007  axpre-suploclemres  8014  axpre-suploc  8015  cnegex  8250  apreap  8660  recexap  8726  sup3exmid  9030  creur  9032  creui  9033  cju  9034  supinfneg  9716  infsupneg  9717  infssuzex  10376  nninfdcex  10380  exbtwnzlemshrink  10391  rebtwn2zlemshrink  10396  modqmuladd  10511  hashunlem  10949  iswrd  10996  csbwrdg  11023  shftfvalg  11129  shftfval  11132  rexfiuz  11300  recvguniq  11306  fimaxre2  11538  clim  11592  sumeq1  11666  summodc  11694  fsum3  11698  mertenslemub  11845  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  prodeq1f  11863  prodeq2w  11867  prodmodc  11889  fprodseq  11894  divides  12100  odd2np1lem  12183  opeo  12208  omeo  12209  divalglemeunn  12232  divalglemeuneg  12234  zeqzmulgcd  12291  bezoutlemnewy  12317  bezoutlemmain  12319  bezoutlemex  12322  bezoutlemaz  12324  exprmfct  12460  nnnn0modprm0  12578  pceu  12618  pcprmpw2  12656  4sqlemafi  12718  4sqexercise1  12721  4sqlem12  12725  ennnfoneleminc  12782  ennnfonelemex  12785  ennnfonelemhom  12786  ennnfonelemnn0  12793  ennnfonelemr  12794  ctinfomlemom  12798  ctinfom  12799  nninfdclemcl  12819  nninfdclemp1  12821  nninfdc  12824  ptex  13096  grpinvalem  13217  igsumvalx  13221  gsumpropd  13224  gsumress  13227  gsum0g  13228  isnsgrp  13238  grpinvex  13342  dfgrp2  13359  grpidinv2  13390  grpidinv  13391  dfgrp3mlem  13430  grp1  13438  imasgrp2  13446  dvdsrd  13856  opprunitd  13872  subrgdvds  13997  lss1d  14145  lspsn  14178  ellspsn  14179  rspsn  14296  znf1o  14413  basis2  14520  eltg2  14525  tg2  14532  neival  14615  isnei  14616  isneip  14618  restbasg  14640  cnpval  14670  iscnp  14671  icnpimaex  14683  lmbr  14685  lmbr2  14686  cnptoprest2  14712  lmff  14721  txbas  14730  txcnp  14743  txrest  14748  blssps  14899  blss  14900  mopni  14954  metss  14966  metrest  14978  metcnp3  14983  divcnap  15037  cncfval  15044  elcncf2  15046  cncfmet  15064  dedekindeulemuub  15089  dedekindeulemloc  15091  dedekindeulemlu  15093  suplociccreex  15096  dedekindicclemuub  15098  dedekindicclemloc  15100  dedekindicclemlu  15102  ivthreinc  15117  limccl  15131  ellimc3apf  15132  limcdifap  15134  limcmpted  15135  plyval  15204  elply2  15207  2lgslem1b  15566  bj-inf2vnlem1  15910  bj-inf2vnlem2  15911  bj-nn0sucALT  15918  sscoll2  15928  subctctexmid  15941  pw1nct  15944  isomninnlem  15973  trilpolemlt1  15984  trirec0  15987  ismkvnnlem  15995