Theorem cbvrexv 2769

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

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

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517

This theorem is referenced by:  cbvrex2v  2782  reu7  3002  reusv3  4563  funcnvuni  5406  fun11iun  5613  fvelimab  5711  fliftfun  5947  tfr1onlemaccex  6557  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemaccex  6570  tfrcldm  6572  frecsuc  6616  nnaordex  6739  fimax2gtri  7134  supmoti  7235  suplub2ti  7243  fodjuomnilemdc  7386  fodjuomnilemres  7390  fodjuomni  7391  fodjumkvlemres  7401  fodjumkv  7402  nninfwlpoimlemginf  7418  nninfwlpoim  7421  nninfinfwlpo  7422  cardval3ex  7432  prarloclemlo  7757  prarloclem3  7760  cauappcvgprlemdisj  7914  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgpr  7925  caucvgprlemdisj  7937  caucvgprlemcl  7939  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgpr  7945  caucvgprprlemell  7948  caucvgprprlemelu  7949  caucvgprprlemlol  7961  caucvgprprlemclphr  7968  caucvgprprlemexbt  7969  suplocexprlemmu  7981  suplocexpr  7988  suplocsrlem  8071  nntopi  8157  axcaucvglemres  8162  axpre-suploc  8165  suprzclex  9622  supinfneg  9873  infsupneg  9874  ublbneg  9891  suprzubdc  10542  exbtwnzlemstep  10553  exbtwnzlemshrink  10554  rebtwn2zlemstep  10558  rebtwn2zlemshrink  10559  hashunlem  11113  cvg1nlemres  11608  resqrexlemoverl  11644  resqrexlemsqa  11647  resqrexlemex  11648  rexanre  11843  rexico  11844  fimaxre2  11850  summodclem2  12006  summodc  12007  mertenslemub  12158  mertensabs  12161  odd2np1lem  12496  divalglemeunn  12545  divalglemeuneg  12547  bitsfzolem  12578  bezoutlemex  12635  ennnfoneleminc  13095  ennnfonelemex  13098  ennnfonelemhom  13099  ennnfonelemr  13107  ctinfom  13112  nninfdclemp1  13134  nninfdc  13137  cnptoprest  15033  dedekindeulemuub  15411  dedekindeulemub  15412  dedekindeulemloc  15413  dedekindeulemlub  15414  dedekindeulemlu  15415  dedekindicclemuub  15420  dedekindicclemub  15421  dedekindicclemloc  15422  dedekindicclemlub  15423  dedekindicclemlu  15424  ivthdich  15447  bj-nn0sucALT  16677  nconstwlpolem  16781  neapmkvlem  16783