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  2998  reusv3  4551  funcnvuni  5390  fun11iun  5593  fvelimab  5690  fliftfun  5920  tfr1onlemaccex  6494  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllemaccex  6507  tfrcldm  6509  frecsuc  6553  nnaordex  6674  fimax2gtri  7063  supmoti  7160  suplub2ti  7168  fodjuomnilemdc  7311  fodjuomnilemres  7315  fodjuomni  7316  fodjumkvlemres  7326  fodjumkv  7327  nninfwlpoimlemginf  7343  nninfwlpoim  7346  nninfinfwlpo  7347  cardval3ex  7357  prarloclemlo  7681  prarloclem3  7684  cauappcvgprlemdisj  7838  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  cauappcvgpr  7849  caucvgprlemdisj  7861  caucvgprlemcl  7863  caucvgprlemladdfu  7864  caucvgprlemladdrl  7865  caucvgpr  7869  caucvgprprlemell  7872  caucvgprprlemelu  7873  caucvgprprlemlol  7885  caucvgprprlemclphr  7892  caucvgprprlemexbt  7893  suplocexprlemmu  7905  suplocexpr  7912  suplocsrlem  7995  nntopi  8081  axcaucvglemres  8086  axpre-suploc  8089  suprzclex  9545  supinfneg  9790  infsupneg  9791  ublbneg  9808  suprzubdc  10456  exbtwnzlemstep  10467  exbtwnzlemshrink  10468  rebtwn2zlemstep  10472  rebtwn2zlemshrink  10473  hashunlem  11026  cvg1nlemres  11496  resqrexlemoverl  11532  resqrexlemsqa  11535  resqrexlemex  11536  rexanre  11731  rexico  11732  fimaxre2  11738  summodclem2  11893  summodc  11894  mertenslemub  12045  mertensabs  12048  odd2np1lem  12383  divalglemeunn  12432  divalglemeuneg  12434  bitsfzolem  12465  bezoutlemex  12522  ennnfoneleminc  12982  ennnfonelemex  12985  ennnfonelemhom  12986  ennnfonelemr  12994  ctinfom  12999  nninfdclemp1  13021  nninfdc  13024  cnptoprest  14913  dedekindeulemuub  15291  dedekindeulemub  15292  dedekindeulemloc  15293  dedekindeulemlub  15294  dedekindeulemlu  15295  dedekindicclemuub  15300  dedekindicclemub  15301  dedekindicclemloc  15302  dedekindicclemlub  15303  dedekindicclemlu  15304  ivthdich  15327  bj-nn0sucALT  16341  nconstwlpolem  16433  neapmkvlem  16435