Theorem cbvrexv 2768

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

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

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516

This theorem is referenced by:  cbvrex2v  2781  reu7  3001  reusv3  4557  funcnvuni  5399  fun11iun  5604  fvelimab  5702  fliftfun  5936  tfr1onlemaccex  6513  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllemaccex  6526  tfrcldm  6528  frecsuc  6572  nnaordex  6695  fimax2gtri  7090  supmoti  7191  suplub2ti  7199  fodjuomnilemdc  7342  fodjuomnilemres  7346  fodjuomni  7347  fodjumkvlemres  7357  fodjumkv  7358  nninfwlpoimlemginf  7374  nninfwlpoim  7377  nninfinfwlpo  7378  cardval3ex  7388  prarloclemlo  7713  prarloclem3  7716  cauappcvgprlemdisj  7870  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgpr  7881  caucvgprlemdisj  7893  caucvgprlemcl  7895  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgpr  7901  caucvgprprlemell  7904  caucvgprprlemelu  7905  caucvgprprlemlol  7917  caucvgprprlemclphr  7924  caucvgprprlemexbt  7925  suplocexprlemmu  7937  suplocexpr  7944  suplocsrlem  8027  nntopi  8113  axcaucvglemres  8118  axpre-suploc  8121  suprzclex  9577  supinfneg  9828  infsupneg  9829  ublbneg  9846  suprzubdc  10495  exbtwnzlemstep  10506  exbtwnzlemshrink  10507  rebtwn2zlemstep  10511  rebtwn2zlemshrink  10512  hashunlem  11066  cvg1nlemres  11545  resqrexlemoverl  11581  resqrexlemsqa  11584  resqrexlemex  11585  rexanre  11780  rexico  11781  fimaxre2  11787  summodclem2  11942  summodc  11943  mertenslemub  12094  mertensabs  12097  odd2np1lem  12432  divalglemeunn  12481  divalglemeuneg  12483  bitsfzolem  12514  bezoutlemex  12571  ennnfoneleminc  13031  ennnfonelemex  13034  ennnfonelemhom  13035  ennnfonelemr  13043  ctinfom  13048  nninfdclemp1  13070  nninfdc  13073  cnptoprest  14962  dedekindeulemuub  15340  dedekindeulemub  15341  dedekindeulemloc  15342  dedekindeulemlub  15343  dedekindeulemlu  15344  dedekindicclemuub  15349  dedekindicclemub  15350  dedekindicclemloc  15351  dedekindicclemlub  15352  dedekindicclemlu  15353  ivthdich  15376  bj-nn0sucALT  16573  nconstwlpolem  16669  neapmkvlem  16671