Theorem cbvrexv 2693

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-cleq 2158  df-clel 2161  df-nfc 2297  df-rex 2450

This theorem is referenced by:  cbvrex2v  2706  reu7  2921  reusv3  4438  funcnvuni  5257  fun11iun  5453  fvelimab  5542  fliftfun  5764  tfr1onlemaccex  6316  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllemaccex  6329  tfrcldm  6331  frecsuc  6375  nnaordex  6495  fimax2gtri  6867  supmoti  6958  suplub2ti  6966  fodjuomnilemdc  7108  fodjuomnilemres  7112  fodjuomni  7113  fodjumkvlemres  7123  fodjumkv  7124  cardval3ex  7141  prarloclemlo  7435  prarloclem3  7438  cauappcvgprlemdisj  7592  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  cauappcvgpr  7603  caucvgprlemdisj  7615  caucvgprlemcl  7617  caucvgprlemladdfu  7618  caucvgprlemladdrl  7619  caucvgpr  7623  caucvgprprlemell  7626  caucvgprprlemelu  7627  caucvgprprlemlol  7639  caucvgprprlemclphr  7646  caucvgprprlemexbt  7647  suplocexprlemmu  7659  suplocexpr  7666  suplocsrlem  7749  nntopi  7835  axcaucvglemres  7840  axpre-suploc  7843  suprzclex  9289  supinfneg  9533  infsupneg  9534  ublbneg  9551  exbtwnzlemstep  10183  exbtwnzlemshrink  10184  rebtwn2zlemstep  10188  rebtwn2zlemshrink  10189  hashunlem  10717  cvg1nlemres  10927  resqrexlemoverl  10963  resqrexlemsqa  10966  resqrexlemex  10967  rexanre  11162  rexico  11163  fimaxre2  11168  summodclem2  11323  summodc  11324  mertenslemub  11475  mertensabs  11478  odd2np1lem  11809  divalglemeunn  11858  divalglemeuneg  11860  suprzubdc  11885  bezoutlemex  11934  ennnfoneleminc  12344  ennnfonelemex  12347  ennnfonelemhom  12348  ennnfonelemr  12356  ctinfom  12361  nninfdclemcl  12381  nninfdclemp1  12383  nninfdc  12386  cnptoprest  12879  dedekindeulemuub  13235  dedekindeulemub  13236  dedekindeulemloc  13237  dedekindeulemlub  13238  dedekindeulemlu  13239  dedekindicclemuub  13244  dedekindicclemub  13245  dedekindicclemloc  13246  dedekindicclemlub  13247  dedekindicclemlu  13248  bj-nn0sucALT  13860  nconstwlpolem  13943  neapmkvlem  13945