Theorem cbvrexv 2743

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

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

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492

This theorem is referenced by:  cbvrex2v  2756  reu7  2975  reusv3  4525  funcnvuni  5362  fun11iun  5565  fvelimab  5658  fliftfun  5888  tfr1onlemaccex  6457  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllemaccex  6470  tfrcldm  6472  frecsuc  6516  nnaordex  6637  fimax2gtri  7024  supmoti  7121  suplub2ti  7129  fodjuomnilemdc  7272  fodjuomnilemres  7276  fodjuomni  7277  fodjumkvlemres  7287  fodjumkv  7288  nninfwlpoimlemginf  7304  nninfwlpoim  7307  nninfinfwlpo  7308  cardval3ex  7318  prarloclemlo  7642  prarloclem3  7645  cauappcvgprlemdisj  7799  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgpr  7810  caucvgprlemdisj  7822  caucvgprlemcl  7824  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  caucvgpr  7830  caucvgprprlemell  7833  caucvgprprlemelu  7834  caucvgprprlemlol  7846  caucvgprprlemclphr  7853  caucvgprprlemexbt  7854  suplocexprlemmu  7866  suplocexpr  7873  suplocsrlem  7956  nntopi  8042  axcaucvglemres  8047  axpre-suploc  8050  suprzclex  9506  supinfneg  9751  infsupneg  9752  ublbneg  9769  suprzubdc  10416  exbtwnzlemstep  10427  exbtwnzlemshrink  10428  rebtwn2zlemstep  10432  rebtwn2zlemshrink  10433  hashunlem  10986  cvg1nlemres  11411  resqrexlemoverl  11447  resqrexlemsqa  11450  resqrexlemex  11451  rexanre  11646  rexico  11647  fimaxre2  11653  summodclem2  11808  summodc  11809  mertenslemub  11960  mertensabs  11963  odd2np1lem  12298  divalglemeunn  12347  divalglemeuneg  12349  bitsfzolem  12380  bezoutlemex  12437  ennnfoneleminc  12897  ennnfonelemex  12900  ennnfonelemhom  12901  ennnfonelemr  12909  ctinfom  12914  nninfdclemp1  12936  nninfdc  12939  cnptoprest  14826  dedekindeulemuub  15204  dedekindeulemub  15205  dedekindeulemloc  15206  dedekindeulemlub  15207  dedekindeulemlu  15208  dedekindicclemuub  15213  dedekindicclemub  15214  dedekindicclemloc  15215  dedekindicclemlub  15216  dedekindicclemlu  15217  ivthdich  15240  bj-nn0sucALT  16113  nconstwlpolem  16206  neapmkvlem  16208