Theorem cbvrexv 2658

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.)

Hypothesis

Ref	Expression
cbvralv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvrexv	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvrexv

Step	Hyp	Ref	Expression
1		nfv 1509	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1509	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvralv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvrex 2654	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 104  ∃wrex 2418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423

This theorem is referenced by:  cbvrexvw  2662  cbvrex2v  2669  reu7  2883  reusv3  4389  funcnvuni  5200  fun11iun  5396  fvelimab  5485  fliftfun  5705  grpridd  5975  tfr1onlemaccex  6253  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllemaccex  6266  tfrcldm  6268  frecsuc  6312  nnaordex  6431  fimax2gtri  6803  supmoti  6888  suplub2ti  6896  fodjuomnilemdc  7024  fodjuomnilemres  7028  fodjuomni  7029  fodjumkvlemres  7041  fodjumkv  7042  cardval3ex  7058  prarloclemlo  7326  prarloclem3  7329  cauappcvgprlemdisj  7483  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgpr  7494  caucvgprlemdisj  7506  caucvgprlemcl  7508  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgpr  7514  caucvgprprlemell  7517  caucvgprprlemelu  7518  caucvgprprlemlol  7530  caucvgprprlemclphr  7537  caucvgprprlemexbt  7538  suplocexprlemmu  7550  suplocexpr  7557  suplocsrlem  7640  nntopi  7726  axcaucvglemres  7731  axpre-suploc  7734  suprzclex  9173  supinfneg  9417  infsupneg  9418  ublbneg  9432  exbtwnzlemstep  10056  exbtwnzlemshrink  10057  rebtwn2zlemstep  10061  rebtwn2zlemshrink  10062  hashunlem  10582  cvg1nlemres  10789  resqrexlemoverl  10825  resqrexlemsqa  10828  resqrexlemex  10829  rexanre  11024  rexico  11025  fimaxre2  11030  summodclem2  11183  summodc  11184  mertenslemub  11335  mertensabs  11338  odd2np1lem  11605  divalglemeunn  11654  divalglemeuneg  11656  bezoutlemex  11725  ennnfoneleminc  11960  ennnfonelemex  11963  ennnfonelemhom  11964  ennnfonelemr  11972  ctinfom  11977  cnptoprest  12447  dedekindeulemuub  12803  dedekindeulemub  12804  dedekindeulemloc  12805  dedekindeulemlub  12806  dedekindeulemlu  12807  dedekindicclemuub  12812  dedekindicclemub  12813  dedekindicclemloc  12814  dedekindicclemlub  12815  dedekindicclemlu  12816  bj-nn0sucALT  13347  neapmkvlem  13424