Theorem cbvrexv 2613

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

Syntax hints:   -> wi 4   <-> wb 104   E.wrex 2376

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-cleq 2093  df-clel 2096  df-nfc 2229  df-rex 2381

This theorem is referenced by:  cbvrex2v  2621  reu7  2832  reusv3  4319  funcnvuni  5128  fun11iun  5322  fvelimab  5409  fliftfun  5629  grpridd  5899  tfr1onlemaccex  6175  tfrcllemsucaccv  6181  tfrcllembxssdm  6183  tfrcllemaccex  6188  tfrcldm  6190  frecsuc  6234  nnaordex  6353  fimax2gtri  6724  supmoti  6795  suplub2ti  6803  fodjuomnilemdc  6928  fodjuomnilemres  6932  fodjuomni  6933  fodjumkvlemres  6944  fodjumkv  6945  cardval3ex  6952  prarloclemlo  7203  prarloclem3  7206  cauappcvgprlemdisj  7360  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  cauappcvgpr  7371  caucvgprlemdisj  7383  caucvgprlemcl  7385  caucvgprlemladdfu  7386  caucvgprlemladdrl  7387  caucvgpr  7391  caucvgprprlemell  7394  caucvgprprlemelu  7395  caucvgprprlemlol  7407  caucvgprprlemclphr  7414  caucvgprprlemexbt  7415  nntopi  7579  axcaucvglemres  7584  suprzclex  9001  supinfneg  9240  infsupneg  9241  ublbneg  9255  exbtwnzlemstep  9866  exbtwnzlemshrink  9867  rebtwn2zlemstep  9871  rebtwn2zlemshrink  9872  hashunlem  10391  cvg1nlemres  10597  resqrexlemoverl  10633  resqrexlemsqa  10636  resqrexlemex  10637  rexanre  10832  rexico  10833  fimaxre2  10837  summodclem2  10990  summodc  10991  mertenslemub  11142  mertensabs  11145  odd2np1lem  11364  divalglemeunn  11413  divalglemeuneg  11415  bezoutlemex  11482  ennnfoneleminc  11716  ennnfonelemex  11719  ennnfonelemhom  11720  ennnfonelemr  11728  ctinfom  11733  cnptoprest  12189  bj-nn0sucALT  12761