Theorem cbvexvw 2069

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2430 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017.)

Hypothesis

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

Assertion

Ref	Expression
cbvexvw	⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

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

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

Proof of Theorem cbvexvw

Step	Hyp	Ref	Expression
1		cbvalvw.1	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	notbid 321	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
3	2	cbvalvw 2068	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
4	3	notbii 323	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5		df-ex 1812	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6		df-ex 1812	. 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
7	4, 5, 6	3bitr4i 306	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  cbvex2vw  2073  mojust  2563  mo4  2591  eujust  2596  cbveuvw  2630  iseqsetvlem  2823  cbvrexvw  3241  euind  3681  reuind  3710  cbvopab1v  5182  cbvopab2v  5183  reusv2lem2  5360  axprg  5394  relop  5827  dmcoss  5956  dmcossOLD  5957  fv3  6903  exfo  7105  cbvoprab3v  7512  zfun  7752  suppimacnv  8194  frrlem1  8307  ac6sfi  9278  brwdom2  9570  ttrclss  9724  ttrclselem2  9730  aceq1  10199  aceq0  10200  aceq3lem  10202  dfac4  10204  kmlem2  10233  kmlem13  10244  axdc4lem  10536  zfac  10541  zfcndun  10703  zfcndac  10707  sup2  12276  supmul  12292  climmo  15729  summo  15888  prodmo  16108  gsumval3eu  20123  elpt  23896  gsumwrd2dccatlem  33684  1arithidomlem1  34113  1arithidom  34115  bnj1185  35469  rmo6  35756  axprALT2  35786  fineqvac  35840  axreg  35851  axregscl  35852  tz9.1regs  35858  satf0op  36228  sat1el2xp  36230  mirimanoffr  36546  cbvrexvw2  37108  cbvoprab1vw  37118  cbvoprab2vw  37119  cbvoprab13vw  37122  mh-regprimbi  37425  bj-bm1.3ii  38071  wl-ax12v2cl  38522  wl-dfclel  38531  fdc  38772  sn-sup2  43648  cpcoll2d  45336  axc11next  45483  fnchoice  46139  ichexmpl1  48644  cbvals  51069