Theorem cbvrexv 2779

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

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

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526

This theorem is referenced by:  cbvrex2v  2792  reu7  3012  reusv3  4581  funcnvuni  5425  fun11iun  5635  fvelimab  5733  fliftfun  5969  tfr1onlemaccex  6579  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllemaccex  6592  tfrcldm  6594  frecsuc  6638  nnaordex  6761  fimax2gtri  7159  supmoti  7284  suplub2ti  7292  fodjuomnilemdc  7435  fodjuomnilemres  7439  fodjuomni  7440  fodjumkvlemres  7450  fodjumkv  7451  nninfwlpoimlemginf  7467  nninfwlpoim  7470  nninfinfwlpo  7471  cardval3ex  7481  prarloclemlo  7809  prarloclem3  7812  cauappcvgprlemdisj  7966  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  cauappcvgpr  7977  caucvgprlemdisj  7989  caucvgprlemcl  7991  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  caucvgpr  7997  caucvgprprlemell  8000  caucvgprprlemelu  8001  caucvgprprlemlol  8013  caucvgprprlemclphr  8020  caucvgprprlemexbt  8021  suplocexprlemmu  8033  suplocexpr  8040  suplocsrlem  8123  nntopi  8209  axcaucvglemres  8214  axpre-suploc  8217  suprzclex  9676  supinfneg  9927  infsupneg  9928  ublbneg  9945  suprzubdc  10596  exbtwnzlemstep  10607  exbtwnzlemshrink  10608  rebtwn2zlemstep  10612  rebtwn2zlemshrink  10613  hashunlem  11168  cvg1nlemres  11670  resqrexlemoverl  11706  resqrexlemsqa  11709  resqrexlemex  11710  rexanre  11905  rexico  11906  fimaxre2  11912  summodclem2  12068  summodc  12069  mertenslemub  12220  mertensabs  12223  odd2np1lem  12558  divalglemeunn  12607  divalglemeuneg  12609  bitsfzolem  12640  bezoutlemex  12697  ennnfoneleminc  13162  ennnfonelemex  13165  ennnfonelemhom  13166  ennnfonelemr  13174  ctinfom  13179  nninfdclemp1  13201  nninfdc  13204  cnptoprest  15104  dedekindeulemuub  15482  dedekindeulemub  15483  dedekindeulemloc  15484  dedekindeulemlub  15485  dedekindeulemlu  15486  dedekindicclemuub  15491  dedekindicclemub  15492  dedekindicclemloc  15493  dedekindicclemlub  15494  dedekindicclemlu  15495  ivthdich  15518  bj-nn0sucALT  16748  nconstwlpolem  16851  neapmkvlem  16853