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  5937  tfr1onlemaccex  6514  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemaccex  6527  tfrcldm  6529  frecsuc  6573  nnaordex  6696  fimax2gtri  7091  supmoti  7192  suplub2ti  7200  fodjuomnilemdc  7343  fodjuomnilemres  7347  fodjuomni  7348  fodjumkvlemres  7358  fodjumkv  7359  nninfwlpoimlemginf  7375  nninfwlpoim  7378  nninfinfwlpo  7379  cardval3ex  7389  prarloclemlo  7714  prarloclem3  7717  cauappcvgprlemdisj  7871  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgpr  7882  caucvgprlemdisj  7894  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemlol  7918  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  suplocexprlemmu  7938  suplocexpr  7945  suplocsrlem  8028  nntopi  8114  axcaucvglemres  8119  axpre-suploc  8122  suprzclex  9578  supinfneg  9829  infsupneg  9830  ublbneg  9847  suprzubdc  10497  exbtwnzlemstep  10508  exbtwnzlemshrink  10509  rebtwn2zlemstep  10513  rebtwn2zlemshrink  10514  hashunlem  11068  cvg1nlemres  11563  resqrexlemoverl  11599  resqrexlemsqa  11602  resqrexlemex  11603  rexanre  11798  rexico  11799  fimaxre2  11805  summodclem2  11961  summodc  11962  mertenslemub  12113  mertensabs  12116  odd2np1lem  12451  divalglemeunn  12500  divalglemeuneg  12502  bitsfzolem  12533  bezoutlemex  12590  ennnfoneleminc  13050  ennnfonelemex  13053  ennnfonelemhom  13054  ennnfonelemr  13062  ctinfom  13067  nninfdclemp1  13089  nninfdc  13092  cnptoprest  14982  dedekindeulemuub  15360  dedekindeulemub  15361  dedekindeulemloc  15362  dedekindeulemlub  15363  dedekindeulemlu  15364  dedekindicclemuub  15369  dedekindicclemub  15370  dedekindicclemloc  15371  dedekindicclemlub  15372  dedekindicclemlu  15373  ivthdich  15396  bj-nn0sucALT  16624  nconstwlpolem  16721  neapmkvlem  16723