Theorem cbvrexv 2787

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   E.wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534

This theorem is used by:  cbvrex2v  2800  reu7  3021  reusv3  4608  funcnvuni  5453  fun11iun  5663  fvelimab  5762  fliftfun  6005  tfr1onlemaccex  6623  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllemaccex  6636  tfrcldm  6638  frecsuc  6682  nnaordex  6805  fimax2gtri  7210  supmoti  7339  suplub2ti  7347  fodjuomnilemdc  7490  fodjuomnilemres  7494  fodjuomni  7495  fodjumkvlemres  7505  fodjumkv  7506  nninfwlpoimlemginf  7522  nninfwlpoim  7525  nninfinfwlpo  7526  cardval3ex  7536  prarloclemlo  7867  prarloclem3  7870  cauappcvgprlemdisj  8024  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgpr  8035  caucvgprlemdisj  8047  caucvgprlemcl  8049  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgpr  8055  caucvgprprlemell  8058  caucvgprprlemelu  8059  caucvgprprlemlol  8071  caucvgprprlemclphr  8078  caucvgprprlemexbt  8079  suplocexprlemmu  8091  suplocexpr  8098  suplocsrlem  8181  nntopi  8267  axcaucvglemres  8272  axpre-suploc  8275  suprzclex  9755  supinfneg  10011  infsupneg  10012  ublbneg  10029  suprzubdc  10688  exbtwnzlemstep  10699  exbtwnzlemshrink  10700  rebtwn2zlemstep  10704  rebtwn2zlemshrink  10705  hashunlem  11266  cvg1nlemres  11773  resqrexlemoverl  11809  resqrexlemsqa  11812  resqrexlemex  11813  rexanre  12009  rexico  12010  fimaxre2  12016  fiidxsupcl  12018  summodclem2  12174  summodc  12175  mertenslemub  12326  mertensabs  12329  odd2np1lem  12664  divalglemeunn  12713  divalglemeuneg  12715  bitsfzolem  12746  bezoutlemex  12803  nn0sqdcq  13013  ballotfilemodife  13298  ballotfilemimin  13307  ennnfoneleminc  13360  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemr  13372  ctinfom  13377  nninfdclemp1  13399  nninfdc  13402  cnptoprest  15465  dedekindeulemuub  15843  dedekindeulemub  15844  dedekindeulemloc  15845  dedekindeulemlub  15846  dedekindeulemlu  15847  dedekindicclemuub  15852  dedekindicclemub  15853  dedekindicclemloc  15854  dedekindicclemlub  15855  dedekindicclemlu  15856  ivthdich  15879  bj-nn0sucALT  17209  nconstwlpolem  17322  neapmkvlem  17324