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  2955  reusv3  4491  funcnvuni  5323  fun11iun  5521  fvelimab  5613  fliftfun  5839  tfr1onlemaccex  6401  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllemaccex  6414  tfrcldm  6416  frecsuc  6460  nnaordex  6581  fimax2gtri  6957  supmoti  7052  suplub2ti  7060  fodjuomnilemdc  7203  fodjuomnilemres  7207  fodjuomni  7208  fodjumkvlemres  7218  fodjumkv  7219  nninfwlpoimlemginf  7235  nninfwlpoim  7237  cardval3ex  7245  prarloclemlo  7554  prarloclem3  7557  cauappcvgprlemdisj  7711  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgpr  7722  caucvgprlemdisj  7734  caucvgprlemcl  7736  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  caucvgpr  7742  caucvgprprlemell  7745  caucvgprprlemelu  7746  caucvgprprlemlol  7758  caucvgprprlemclphr  7765  caucvgprprlemexbt  7766  suplocexprlemmu  7778  suplocexpr  7785  suplocsrlem  7868  nntopi  7954  axcaucvglemres  7959  axpre-suploc  7962  suprzclex  9415  supinfneg  9660  infsupneg  9661  ublbneg  9678  exbtwnzlemstep  10316  exbtwnzlemshrink  10317  rebtwn2zlemstep  10321  rebtwn2zlemshrink  10322  hashunlem  10875  cvg1nlemres  11129  resqrexlemoverl  11165  resqrexlemsqa  11168  resqrexlemex  11169  rexanre  11364  rexico  11365  fimaxre2  11370  summodclem2  11525  summodc  11526  mertenslemub  11677  mertensabs  11680  odd2np1lem  12013  divalglemeunn  12062  divalglemeuneg  12064  suprzubdc  12089  bezoutlemex  12138  ennnfoneleminc  12568  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemr  12580  ctinfom  12585  nninfdclemp1  12607  nninfdc  12610  cnptoprest  14407  dedekindeulemuub  14771  dedekindeulemub  14772  dedekindeulemloc  14773  dedekindeulemlub  14774  dedekindeulemlu  14775  dedekindicclemuub  14780  dedekindicclemub  14781  dedekindicclemloc  14782  dedekindicclemlub  14783  dedekindicclemlu  14784  ivthdich  14807  bj-nn0sucALT  15470  nconstwlpolem  15555  neapmkvlem  15557