Theorem cbvrexv 2706

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

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

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461

This theorem is referenced by:  cbvrex2v  2719  reu7  2934  reusv3  4462  funcnvuni  5287  fun11iun  5484  fvelimab  5574  fliftfun  5799  tfr1onlemaccex  6351  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllemaccex  6364  tfrcldm  6366  frecsuc  6410  nnaordex  6531  fimax2gtri  6903  supmoti  6994  suplub2ti  7002  fodjuomnilemdc  7144  fodjuomnilemres  7148  fodjuomni  7149  fodjumkvlemres  7159  fodjumkv  7160  nninfwlpoimlemginf  7176  nninfwlpoim  7178  cardval3ex  7186  prarloclemlo  7495  prarloclem3  7498  cauappcvgprlemdisj  7652  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  cauappcvgpr  7663  caucvgprlemdisj  7675  caucvgprlemcl  7677  caucvgprlemladdfu  7678  caucvgprlemladdrl  7679  caucvgpr  7683  caucvgprprlemell  7686  caucvgprprlemelu  7687  caucvgprprlemlol  7699  caucvgprprlemclphr  7706  caucvgprprlemexbt  7707  suplocexprlemmu  7719  suplocexpr  7726  suplocsrlem  7809  nntopi  7895  axcaucvglemres  7900  axpre-suploc  7903  suprzclex  9353  supinfneg  9597  infsupneg  9598  ublbneg  9615  exbtwnzlemstep  10250  exbtwnzlemshrink  10251  rebtwn2zlemstep  10255  rebtwn2zlemshrink  10256  hashunlem  10786  cvg1nlemres  10996  resqrexlemoverl  11032  resqrexlemsqa  11035  resqrexlemex  11036  rexanre  11231  rexico  11232  fimaxre2  11237  summodclem2  11392  summodc  11393  mertenslemub  11544  mertensabs  11547  odd2np1lem  11879  divalglemeunn  11928  divalglemeuneg  11930  suprzubdc  11955  bezoutlemex  12004  ennnfoneleminc  12414  ennnfonelemex  12417  ennnfonelemhom  12418  ennnfonelemr  12426  ctinfom  12431  nninfdclemcl  12451  nninfdclemp1  12453  nninfdc  12456  cnptoprest  13778  dedekindeulemuub  14134  dedekindeulemub  14135  dedekindeulemloc  14136  dedekindeulemlub  14137  dedekindeulemlu  14138  dedekindicclemuub  14143  dedekindicclemub  14144  dedekindicclemloc  14145  dedekindicclemlub  14146  dedekindicclemlu  14147  bj-nn0sucALT  14769  nconstwlpolem  14852  neapmkvlem  14854