Theorem cbvrexv 2727

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

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

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478

This theorem is referenced by:  cbvrex2v  2740  reu7  2956  reusv3  4492  funcnvuni  5324  fun11iun  5522  fvelimab  5614  fliftfun  5840  tfr1onlemaccex  6403  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllemaccex  6416  tfrcldm  6418  frecsuc  6462  nnaordex  6583  fimax2gtri  6959  supmoti  7054  suplub2ti  7062  fodjuomnilemdc  7205  fodjuomnilemres  7209  fodjuomni  7210  fodjumkvlemres  7220  fodjumkv  7221  nninfwlpoimlemginf  7237  nninfwlpoim  7239  cardval3ex  7247  prarloclemlo  7556  prarloclem3  7559  cauappcvgprlemdisj  7713  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgpr  7724  caucvgprlemdisj  7736  caucvgprlemcl  7738  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgpr  7744  caucvgprprlemell  7747  caucvgprprlemelu  7748  caucvgprprlemlol  7760  caucvgprprlemclphr  7767  caucvgprprlemexbt  7768  suplocexprlemmu  7780  suplocexpr  7787  suplocsrlem  7870  nntopi  7956  axcaucvglemres  7961  axpre-suploc  7964  suprzclex  9418  supinfneg  9663  infsupneg  9664  ublbneg  9681  exbtwnzlemstep  10319  exbtwnzlemshrink  10320  rebtwn2zlemstep  10324  rebtwn2zlemshrink  10325  hashunlem  10878  cvg1nlemres  11132  resqrexlemoverl  11168  resqrexlemsqa  11171  resqrexlemex  11172  rexanre  11367  rexico  11368  fimaxre2  11373  summodclem2  11528  summodc  11529  mertenslemub  11680  mertensabs  11683  odd2np1lem  12016  divalglemeunn  12065  divalglemeuneg  12067  suprzubdc  12092  bezoutlemex  12141  ennnfoneleminc  12571  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemr  12583  ctinfom  12588  nninfdclemp1  12610  nninfdc  12613  cnptoprest  14418  dedekindeulemuub  14796  dedekindeulemub  14797  dedekindeulemloc  14798  dedekindeulemlub  14799  dedekindeulemlu  14800  dedekindicclemuub  14805  dedekindicclemub  14806  dedekindicclemloc  14807  dedekindicclemlub  14808  dedekindicclemlu  14809  ivthdich  14832  bj-nn0sucALT  15540  nconstwlpolem  15625  neapmkvlem  15627