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  6624  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllemaccex  6637  tfrcldm  6639  frecsuc  6683  nnaordex  6806  fimax2gtri  7212  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  9754  supinfneg  10010  infsupneg  10011  ublbneg  10028  suprzubdc  10687  exbtwnzlemstep  10698  exbtwnzlemshrink  10699  rebtwn2zlemstep  10703  rebtwn2zlemshrink  10704  hashunlem  11265  cvg1nlemres  11772  resqrexlemoverl  11808  resqrexlemsqa  11811  resqrexlemex  11812  rexanre  12008  rexico  12009  fimaxre2  12015  fiidxsupcl  12017  summodclem2  12173  summodc  12174  mertenslemub  12325  mertensabs  12328  odd2np1lem  12663  divalglemeunn  12712  divalglemeuneg  12714  bitsfzolem  12745  bezoutlemex  12802  nn0sqdcq  13012  ballotfilemodife  13297  ballotfilemimin  13306  ennnfoneleminc  13359  ennnfonelemex  13362  ennnfonelemhom  13363  ennnfonelemr  13371  ctinfom  13376  nninfdclemp1  13398  nninfdc  13401  psrbagmaxlem1  15178  cnptoprest  15482  dedekindeulemuub  15860  dedekindeulemub  15861  dedekindeulemloc  15862  dedekindeulemlub  15863  dedekindeulemlu  15864  dedekindicclemuub  15869  dedekindicclemub  15870  dedekindicclemloc  15871  dedekindicclemlub  15872  dedekindicclemlu  15873  ivthdich  15896  bj-nn0sucALT  17226  nconstwlpolem  17339  neapmkvlem  17341