Theorem cbvrexv 2704

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

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

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461

This theorem is referenced by:  cbvrex2v  2717  reu7  2932  reusv3  4460  funcnvuni  5285  fun11iun  5482  fvelimab  5572  fliftfun  5796  tfr1onlemaccex  6348  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllemaccex  6361  tfrcldm  6363  frecsuc  6407  nnaordex  6528  fimax2gtri  6900  supmoti  6991  suplub2ti  6999  fodjuomnilemdc  7141  fodjuomnilemres  7145  fodjuomni  7146  fodjumkvlemres  7156  fodjumkv  7157  nninfwlpoimlemginf  7173  nninfwlpoim  7175  cardval3ex  7183  prarloclemlo  7492  prarloclem3  7495  cauappcvgprlemdisj  7649  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  cauappcvgpr  7660  caucvgprlemdisj  7672  caucvgprlemcl  7674  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgpr  7680  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemlol  7696  caucvgprprlemclphr  7703  caucvgprprlemexbt  7704  suplocexprlemmu  7716  suplocexpr  7723  suplocsrlem  7806  nntopi  7892  axcaucvglemres  7897  axpre-suploc  7900  suprzclex  9349  supinfneg  9593  infsupneg  9594  ublbneg  9611  exbtwnzlemstep  10245  exbtwnzlemshrink  10246  rebtwn2zlemstep  10250  rebtwn2zlemshrink  10251  hashunlem  10779  cvg1nlemres  10989  resqrexlemoverl  11025  resqrexlemsqa  11028  resqrexlemex  11029  rexanre  11224  rexico  11225  fimaxre2  11230  summodclem2  11385  summodc  11386  mertenslemub  11537  mertensabs  11540  odd2np1lem  11871  divalglemeunn  11920  divalglemeuneg  11922  suprzubdc  11947  bezoutlemex  11996  ennnfoneleminc  12406  ennnfonelemex  12409  ennnfonelemhom  12410  ennnfonelemr  12418  ctinfom  12423  nninfdclemcl  12443  nninfdclemp1  12445  nninfdc  12448  cnptoprest  13632  dedekindeulemuub  13988  dedekindeulemub  13989  dedekindeulemloc  13990  dedekindeulemlub  13991  dedekindeulemlu  13992  dedekindicclemuub  13997  dedekindicclemub  13998  dedekindicclemloc  13999  dedekindicclemlub  14000  dedekindicclemlu  14001  bj-nn0sucALT  14612  nconstwlpolem  14694  neapmkvlem  14696