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 )

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

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 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 theorem 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 referenced by:  cbvrex2v  2800  reu7  3021  reusv3  4601  funcnvuni  5445  fun11iun  5655  fvelimab  5753  fliftfun  5992  tfr1onlemaccex  6609  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllemaccex  6622  tfrcldm  6624  frecsuc  6668  nnaordex  6791  fimax2gtri  7196  supmoti  7323  suplub2ti  7331  fodjuomnilemdc  7474  fodjuomnilemres  7478  fodjuomni  7479  fodjumkvlemres  7489  fodjumkv  7490  nninfwlpoimlemginf  7506  nninfwlpoim  7509  nninfinfwlpo  7510  cardval3ex  7520  prarloclemlo  7851  prarloclem3  7854  cauappcvgprlemdisj  8008  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgpr  8019  caucvgprlemdisj  8031  caucvgprlemcl  8033  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  caucvgpr  8039  caucvgprprlemell  8042  caucvgprprlemelu  8043  caucvgprprlemlol  8055  caucvgprprlemclphr  8062  caucvgprprlemexbt  8063  suplocexprlemmu  8075  suplocexpr  8082  suplocsrlem  8165  nntopi  8251  axcaucvglemres  8256  axpre-suploc  8259  suprzclex  9723  supinfneg  9974  infsupneg  9975  ublbneg  9992  suprzubdc  10649  exbtwnzlemstep  10660  exbtwnzlemshrink  10661  rebtwn2zlemstep  10665  rebtwn2zlemshrink  10666  hashunlem  11222  cvg1nlemres  11729  resqrexlemoverl  11765  resqrexlemsqa  11768  resqrexlemex  11769  rexanre  11964  rexico  11965  fimaxre2  11971  summodclem2  12127  summodc  12128  mertenslemub  12279  mertensabs  12282  odd2np1lem  12617  divalglemeunn  12666  divalglemeuneg  12668  bitsfzolem  12699  bezoutlemex  12756  ballotfilemodife  13218  ballotfilemimin  13227  ennnfoneleminc  13280  ennnfonelemex  13283  ennnfonelemhom  13284  ennnfonelemr  13292  ctinfom  13297  nninfdclemp1  13319  nninfdc  13322  cnptoprest  15263  dedekindeulemuub  15641  dedekindeulemub  15642  dedekindeulemloc  15643  dedekindeulemlub  15644  dedekindeulemlu  15645  dedekindicclemuub  15650  dedekindicclemub  15651  dedekindicclemloc  15652  dedekindicclemlub  15653  dedekindicclemlu  15654  ivthdich  15677  bj-nn0sucALT  16918  nconstwlpolem  17020  neapmkvlem  17022