Theorem cbvrexv 2766

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

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

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514

This theorem is referenced by:  cbvrex2v  2779  reu7  2999  reusv3  4555  funcnvuni  5396  fun11iun  5601  fvelimab  5698  fliftfun  5932  tfr1onlemaccex  6509  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllemaccex  6522  tfrcldm  6524  frecsuc  6568  nnaordex  6691  fimax2gtri  7084  supmoti  7183  suplub2ti  7191  fodjuomnilemdc  7334  fodjuomnilemres  7338  fodjuomni  7339  fodjumkvlemres  7349  fodjumkv  7350  nninfwlpoimlemginf  7366  nninfwlpoim  7369  nninfinfwlpo  7370  cardval3ex  7380  prarloclemlo  7704  prarloclem3  7707  cauappcvgprlemdisj  7861  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgpr  7872  caucvgprlemdisj  7884  caucvgprlemcl  7886  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  caucvgpr  7892  caucvgprprlemell  7895  caucvgprprlemelu  7896  caucvgprprlemlol  7908  caucvgprprlemclphr  7915  caucvgprprlemexbt  7916  suplocexprlemmu  7928  suplocexpr  7935  suplocsrlem  8018  nntopi  8104  axcaucvglemres  8109  axpre-suploc  8112  suprzclex  9568  supinfneg  9819  infsupneg  9820  ublbneg  9837  suprzubdc  10486  exbtwnzlemstep  10497  exbtwnzlemshrink  10498  rebtwn2zlemstep  10502  rebtwn2zlemshrink  10503  hashunlem  11057  cvg1nlemres  11536  resqrexlemoverl  11572  resqrexlemsqa  11575  resqrexlemex  11576  rexanre  11771  rexico  11772  fimaxre2  11778  summodclem2  11933  summodc  11934  mertenslemub  12085  mertensabs  12088  odd2np1lem  12423  divalglemeunn  12472  divalglemeuneg  12474  bitsfzolem  12505  bezoutlemex  12562  ennnfoneleminc  13022  ennnfonelemex  13025  ennnfonelemhom  13026  ennnfonelemr  13034  ctinfom  13039  nninfdclemp1  13061  nninfdc  13064  cnptoprest  14953  dedekindeulemuub  15331  dedekindeulemub  15332  dedekindeulemloc  15333  dedekindeulemlub  15334  dedekindeulemlu  15335  dedekindicclemuub  15340  dedekindicclemub  15341  dedekindicclemloc  15342  dedekindicclemlub  15343  dedekindicclemlu  15344  ivthdich  15367  bj-nn0sucALT  16509  nconstwlpolem  16605  neapmkvlem  16607