Theorem cbvrexv 2738

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.)

Hypothesis

Ref	Expression
cbvralv.1	|- ( x = y -> ( ph <-> ps ) )

Assertion

Ref	Expression
cbvrexv	|- ( E. x e. A ph <-> E. y e. A ps )

Distinct variable groups:   x, A   y, A   ph, y   ps, x

Allowed substitution hints:   ph( x)   ps( y)

Proof of Theorem cbvrexv

Step	Hyp	Ref	Expression
1		nfv 1550	. 2 |- F/ y ph
2		nfv 1550	. 2 |- F/ x ps
3		cbvralv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
4	1, 2, 3	cbvrex 2734	1 |- ( E. x e. A ph <-> E. y e. A ps )

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

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-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489

This theorem is referenced by:  cbvrex2v  2751  reu7  2967  reusv3  4506  funcnvuni  5342  fun11iun  5542  fvelimab  5634  fliftfun  5864  tfr1onlemaccex  6433  tfrcllemsucaccv  6439  tfrcllembxssdm  6441  tfrcllemaccex  6446  tfrcldm  6448  frecsuc  6492  nnaordex  6613  fimax2gtri  6997  supmoti  7094  suplub2ti  7102  fodjuomnilemdc  7245  fodjuomnilemres  7249  fodjuomni  7250  fodjumkvlemres  7260  fodjumkv  7261  nninfwlpoimlemginf  7277  nninfwlpoim  7280  nninfinfwlpo  7281  cardval3ex  7291  prarloclemlo  7606  prarloclem3  7609  cauappcvgprlemdisj  7763  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  cauappcvgpr  7774  caucvgprlemdisj  7786  caucvgprlemcl  7788  caucvgprlemladdfu  7789  caucvgprlemladdrl  7790  caucvgpr  7794  caucvgprprlemell  7797  caucvgprprlemelu  7798  caucvgprprlemlol  7810  caucvgprprlemclphr  7817  caucvgprprlemexbt  7818  suplocexprlemmu  7830  suplocexpr  7837  suplocsrlem  7920  nntopi  8006  axcaucvglemres  8011  axpre-suploc  8014  suprzclex  9470  supinfneg  9715  infsupneg  9716  ublbneg  9733  suprzubdc  10377  exbtwnzlemstep  10388  exbtwnzlemshrink  10389  rebtwn2zlemstep  10393  rebtwn2zlemshrink  10394  hashunlem  10947  cvg1nlemres  11267  resqrexlemoverl  11303  resqrexlemsqa  11306  resqrexlemex  11307  rexanre  11502  rexico  11503  fimaxre2  11509  summodclem2  11664  summodc  11665  mertenslemub  11816  mertensabs  11819  odd2np1lem  12154  divalglemeunn  12203  divalglemeuneg  12205  bitsfzolem  12236  bezoutlemex  12293  ennnfoneleminc  12753  ennnfonelemex  12756  ennnfonelemhom  12757  ennnfonelemr  12765  ctinfom  12770  nninfdclemp1  12792  nninfdc  12795  cnptoprest  14682  dedekindeulemuub  15060  dedekindeulemub  15061  dedekindeulemloc  15062  dedekindeulemlub  15063  dedekindeulemlu  15064  dedekindicclemuub  15069  dedekindicclemub  15070  dedekindicclemloc  15071  dedekindicclemlub  15072  dedekindicclemlu  15073  ivthdich  15096  bj-nn0sucALT  15876  nconstwlpolem  15966  neapmkvlem  15968