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  6624  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllemaccex  6637  tfrcldm  6639  frecsuc  6683  nnaordex  6806  fimax2gtri  7212  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  9755  supinfneg  10011  infsupneg  10012  ublbneg  10029  suprzubdc  10688  exbtwnzlemstep  10699  exbtwnzlemshrink  10700  rebtwn2zlemstep  10704  rebtwn2zlemshrink  10705  hashunlem  11266  cvg1nlemres  11773  resqrexlemoverl  11809  resqrexlemsqa  11812  resqrexlemex  11813  rexanre  12009  rexico  12010  fimaxre2  12016  fiidxsupcl  12018  summodclem2  12174  summodc  12175  mertenslemub  12326  mertensabs  12329  odd2np1lem  12664  divalglemeunn  12713  divalglemeuneg  12715  bitsfzolem  12746  bezoutlemex  12803  nn0sqdcq  13013  ballotfilemodife  13298  ballotfilemimin  13307  ennnfoneleminc  13360  ennnfonelemex  13363  ennnfonelemhom  13364  ennnfonelemr  13372  ctinfom  13377  nninfdclemp1  13399  nninfdc  13402  psrbagmaxlem1  15185  cnptoprest  15498  dedekindeulemuub  15876  dedekindeulemub  15877  dedekindeulemloc  15878  dedekindeulemlub  15879  dedekindeulemlu  15880  dedekindicclemuub  15885  dedekindicclemub  15886  dedekindicclemloc  15887  dedekindicclemlub  15888  dedekindicclemlu  15889  ivthdich  15912  bj-nn0sucALT  17242  nconstwlpolem  17355  neapmkvlem  17357