Theorem cbvrexv 2768

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

Syntax hints:   → wi 4   ↔ wb 105  ∃wrex 2511

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516

This theorem is referenced by:  cbvrex2v  2781  reu7  3001  reusv3  4557  funcnvuni  5399  fun11iun  5604  fvelimab  5702  fliftfun  5937  tfr1onlemaccex  6514  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemaccex  6527  tfrcldm  6529  frecsuc  6573  nnaordex  6696  fimax2gtri  7091  supmoti  7192  suplub2ti  7200  fodjuomnilemdc  7343  fodjuomnilemres  7347  fodjuomni  7348  fodjumkvlemres  7358  fodjumkv  7359  nninfwlpoimlemginf  7375  nninfwlpoim  7378  nninfinfwlpo  7379  cardval3ex  7389  prarloclemlo  7714  prarloclem3  7717  cauappcvgprlemdisj  7871  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgpr  7882  caucvgprlemdisj  7894  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemelu  7906  caucvgprprlemlol  7918  caucvgprprlemclphr  7925  caucvgprprlemexbt  7926  suplocexprlemmu  7938  suplocexpr  7945  suplocsrlem  8028  nntopi  8114  axcaucvglemres  8119  axpre-suploc  8122  suprzclex  9578  supinfneg  9829  infsupneg  9830  ublbneg  9847  suprzubdc  10497  exbtwnzlemstep  10508  exbtwnzlemshrink  10509  rebtwn2zlemstep  10513  rebtwn2zlemshrink  10514  hashunlem  11068  cvg1nlemres  11550  resqrexlemoverl  11586  resqrexlemsqa  11589  resqrexlemex  11590  rexanre  11785  rexico  11786  fimaxre2  11792  summodclem2  11948  summodc  11949  mertenslemub  12100  mertensabs  12103  odd2np1lem  12438  divalglemeunn  12487  divalglemeuneg  12489  bitsfzolem  12520  bezoutlemex  12577  ennnfoneleminc  13037  ennnfonelemex  13040  ennnfonelemhom  13041  ennnfonelemr  13049  ctinfom  13054  nninfdclemp1  13076  nninfdc  13079  cnptoprest  14969  dedekindeulemuub  15347  dedekindeulemub  15348  dedekindeulemloc  15349  dedekindeulemlub  15350  dedekindeulemlu  15351  dedekindicclemuub  15356  dedekindicclemub  15357  dedekindicclemloc  15358  dedekindicclemlub  15359  dedekindicclemlu  15360  ivthdich  15383  bj-nn0sucALT  16599  nconstwlpolem  16695  neapmkvlem  16697