Theorem cbvrexv 2739

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 1551	. 2 |- F/ y ph
2		nfv 1551	. 2 |- F/ x ps
3		cbvralv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
4	1, 2, 3	cbvrex 2735	1 |- ( E. x e. A ph <-> E. y e. A ps )

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-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490

This theorem is referenced by:  cbvrex2v  2752  reu7  2968  reusv3  4507  funcnvuni  5343  fun11iun  5543  fvelimab  5635  fliftfun  5865  tfr1onlemaccex  6434  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllemaccex  6447  tfrcldm  6449  frecsuc  6493  nnaordex  6614  fimax2gtri  6998  supmoti  7095  suplub2ti  7103  fodjuomnilemdc  7246  fodjuomnilemres  7250  fodjuomni  7251  fodjumkvlemres  7261  fodjumkv  7262  nninfwlpoimlemginf  7278  nninfwlpoim  7281  nninfinfwlpo  7282  cardval3ex  7292  prarloclemlo  7607  prarloclem3  7610  cauappcvgprlemdisj  7764  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgpr  7775  caucvgprlemdisj  7787  caucvgprlemcl  7789  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  caucvgpr  7795  caucvgprprlemell  7798  caucvgprprlemelu  7799  caucvgprprlemlol  7811  caucvgprprlemclphr  7818  caucvgprprlemexbt  7819  suplocexprlemmu  7831  suplocexpr  7838  suplocsrlem  7921  nntopi  8007  axcaucvglemres  8012  axpre-suploc  8015  suprzclex  9471  supinfneg  9716  infsupneg  9717  ublbneg  9734  suprzubdc  10379  exbtwnzlemstep  10390  exbtwnzlemshrink  10391  rebtwn2zlemstep  10395  rebtwn2zlemshrink  10396  hashunlem  10949  cvg1nlemres  11296  resqrexlemoverl  11332  resqrexlemsqa  11335  resqrexlemex  11336  rexanre  11531  rexico  11532  fimaxre2  11538  summodclem2  11693  summodc  11694  mertenslemub  11845  mertensabs  11848  odd2np1lem  12183  divalglemeunn  12232  divalglemeuneg  12234  bitsfzolem  12265  bezoutlemex  12322  ennnfoneleminc  12782  ennnfonelemex  12785  ennnfonelemhom  12786  ennnfonelemr  12794  ctinfom  12799  nninfdclemp1  12821  nninfdc  12824  cnptoprest  14711  dedekindeulemuub  15089  dedekindeulemub  15090  dedekindeulemloc  15091  dedekindeulemlub  15092  dedekindeulemlu  15093  dedekindicclemuub  15098  dedekindicclemub  15099  dedekindicclemloc  15100  dedekindicclemlub  15101  dedekindicclemlu  15102  ivthdich  15125  bj-nn0sucALT  15914  nconstwlpolem  16004  neapmkvlem  16006