Theorem cbvrexv 2692

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 1516	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1516	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvralv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvrex 2688	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

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

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449

This theorem is referenced by:  cbvrex2v  2705  reu7  2920  reusv3  4437  funcnvuni  5256  fun11iun  5452  fvelimab  5541  fliftfun  5763  grpridd  6034  tfr1onlemaccex  6312  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllemaccex  6325  tfrcldm  6327  frecsuc  6371  nnaordex  6491  fimax2gtri  6863  supmoti  6954  suplub2ti  6962  fodjuomnilemdc  7104  fodjuomnilemres  7108  fodjuomni  7109  fodjumkvlemres  7119  fodjumkv  7120  cardval3ex  7137  prarloclemlo  7431  prarloclem3  7434  cauappcvgprlemdisj  7588  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgpr  7599  caucvgprlemdisj  7611  caucvgprlemcl  7613  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgpr  7619  caucvgprprlemell  7622  caucvgprprlemelu  7623  caucvgprprlemlol  7635  caucvgprprlemclphr  7642  caucvgprprlemexbt  7643  suplocexprlemmu  7655  suplocexpr  7662  suplocsrlem  7745  nntopi  7831  axcaucvglemres  7836  axpre-suploc  7839  suprzclex  9285  supinfneg  9529  infsupneg  9530  ublbneg  9547  exbtwnzlemstep  10179  exbtwnzlemshrink  10180  rebtwn2zlemstep  10184  rebtwn2zlemshrink  10185  hashunlem  10713  cvg1nlemres  10923  resqrexlemoverl  10959  resqrexlemsqa  10962  resqrexlemex  10963  rexanre  11158  rexico  11159  fimaxre2  11164  summodclem2  11319  summodc  11320  mertenslemub  11471  mertensabs  11474  odd2np1lem  11805  divalglemeunn  11854  divalglemeuneg  11856  suprzubdc  11881  bezoutlemex  11930  ennnfoneleminc  12340  ennnfonelemex  12343  ennnfonelemhom  12344  ennnfonelemr  12352  ctinfom  12357  nninfdclemcl  12377  nninfdclemp1  12379  nninfdc  12382  cnptoprest  12839  dedekindeulemuub  13195  dedekindeulemub  13196  dedekindeulemloc  13197  dedekindeulemlub  13198  dedekindeulemlu  13199  dedekindicclemuub  13204  dedekindicclemub  13205  dedekindicclemloc  13206  dedekindicclemlub  13207  dedekindicclemlu  13208  bj-nn0sucALT  13820  nconstwlpolem  13903  neapmkvlem  13905