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  4550  funcnvuni  5389  fun11iun  5592  fvelimab  5689  fliftfun  5919  tfr1onlemaccex  6492  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllemaccex  6505  tfrcldm  6507  frecsuc  6551  nnaordex  6672  fimax2gtri  7059  supmoti  7156  suplub2ti  7164  fodjuomnilemdc  7307  fodjuomnilemres  7311  fodjuomni  7312  fodjumkvlemres  7322  fodjumkv  7323  nninfwlpoimlemginf  7339  nninfwlpoim  7342  nninfinfwlpo  7343  cardval3ex  7353  prarloclemlo  7677  prarloclem3  7680  cauappcvgprlemdisj  7834  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  cauappcvgpr  7845  caucvgprlemdisj  7857  caucvgprlemcl  7859  caucvgprlemladdfu  7860  caucvgprlemladdrl  7861  caucvgpr  7865  caucvgprprlemell  7868  caucvgprprlemelu  7869  caucvgprprlemlol  7881  caucvgprprlemclphr  7888  caucvgprprlemexbt  7889  suplocexprlemmu  7901  suplocexpr  7908  suplocsrlem  7991  nntopi  8077  axcaucvglemres  8082  axpre-suploc  8085  suprzclex  9541  supinfneg  9786  infsupneg  9787  ublbneg  9804  suprzubdc  10451  exbtwnzlemstep  10462  exbtwnzlemshrink  10463  rebtwn2zlemstep  10467  rebtwn2zlemshrink  10468  hashunlem  11021  cvg1nlemres  11491  resqrexlemoverl  11527  resqrexlemsqa  11530  resqrexlemex  11531  rexanre  11726  rexico  11727  fimaxre2  11733  summodclem2  11888  summodc  11889  mertenslemub  12040  mertensabs  12043  odd2np1lem  12378  divalglemeunn  12427  divalglemeuneg  12429  bitsfzolem  12460  bezoutlemex  12517  ennnfoneleminc  12977  ennnfonelemex  12980  ennnfonelemhom  12981  ennnfonelemr  12989  ctinfom  12994  nninfdclemp1  13016  nninfdc  13019  cnptoprest  14907  dedekindeulemuub  15285  dedekindeulemub  15286  dedekindeulemloc  15287  dedekindeulemlub  15288  dedekindeulemlu  15289  dedekindicclemuub  15294  dedekindicclemub  15295  dedekindicclemloc  15296  dedekindicclemlub  15297  dedekindicclemlu  15298  ivthdich  15321  bj-nn0sucALT  16299  nconstwlpolem  16392  neapmkvlem  16394