Theorem cbvrexv 2787

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534

This theorem is used by:  cbvrex2v  2800  reu7  3021  reusv3  4608  funcnvuni  5453  fun11iun  5663  fvelimab  5762  fliftfun  6005  tfr1onlemaccex  6623  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllemaccex  6636  tfrcldm  6638  frecsuc  6682  nnaordex  6805  fimax2gtri  7211  supmoti  7340  suplub2ti  7348  fodjuomnilemdc  7491  fodjuomnilemres  7495  fodjuomni  7496  fodjumkvlemres  7506  fodjumkv  7507  nninfwlpoimlemginf  7523  nninfwlpoim  7526  nninfinfwlpo  7527  cardval3ex  7537  prarloclemlo  7868  prarloclem3  7871  cauappcvgprlemdisj  8025  cauappcvgprlemladdru  8030  cauappcvgprlemladdrl  8031  cauappcvgpr  8036  caucvgprlemdisj  8048  caucvgprlemcl  8050  caucvgprlemladdfu  8051  caucvgprlemladdrl  8052  caucvgpr  8056  caucvgprprlemell  8059  caucvgprprlemelu  8060  caucvgprprlemlol  8072  caucvgprprlemclphr  8079  caucvgprprlemexbt  8080  suplocexprlemmu  8092  suplocexpr  8099  suplocsrlem  8182  nntopi  8268  axcaucvglemres  8273  axpre-suploc  8276  suprzclex  9756  supinfneg  10012  infsupneg  10013  ublbneg  10030  suprzubdc  10689  exbtwnzlemstep  10700  exbtwnzlemshrink  10701  rebtwn2zlemstep  10705  rebtwn2zlemshrink  10706  hashunlem  11267  cvg1nlemres  11774  resqrexlemoverl  11810  resqrexlemsqa  11813  resqrexlemex  11814  rexanre  12010  rexico  12011  fimaxre2  12017  fiidxsupcl  12019  summodclem2  12175  summodc  12176  mertenslemub  12327  mertensabs  12330  odd2np1lem  12665  divalglemeunn  12714  divalglemeuneg  12716  bitsfzolem  12747  bezoutlemex  12804  nn0sqdcq  13014  ballotfilemodife  13299  ballotfilemimin  13308  ennnfoneleminc  13361  ennnfonelemex  13364  ennnfonelemhom  13365  ennnfonelemr  13373  ctinfom  13378  nninfdclemp1  13400  nninfdc  13403  cnptoprest  15477  dedekindeulemuub  15855  dedekindeulemub  15856  dedekindeulemloc  15857  dedekindeulemlub  15858  dedekindeulemlu  15859  dedekindicclemuub  15864  dedekindicclemub  15865  dedekindicclemloc  15866  dedekindicclemlub  15867  dedekindicclemlu  15868  ivthdich  15891  bj-nn0sucALT  17221  nconstwlpolem  17334  neapmkvlem  17336