Theorem cbvexvw 2056

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2431 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 320	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
3	2	cbvalvw 2055	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
4	3	notbii 322	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5		df-ex 1799	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6		df-ex 1799	. 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
7	4, 5, 6	3bitr4i 305	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208  ∀wal 1557  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799

This theorem is referenced by:  cbvex2vw  2060  mojust  2564  mo4  2592  eujust  2597  cbveuvw  2631  iseqsetvlem  2824  cbvrexvw  3240  euind  3686  reuind  3715  cbvopab1v  5177  cbvopab2v  5178  bm1.3iiOLD  5251  reusv2lem2  5355  axprg  5393  relop  5820  dmcoss  5949  dmcossOLD  5950  fv3  6881  exfo  7082  cbvoprab3v  7484  zfun  7715  suppimacnv  8149  frrlem1  8262  ac6sfi  9224  brwdom2  9518  ttrclss  9672  ttrclselem2  9678  aceq1  10070  aceq0  10071  aceq3lem  10073  dfac4  10075  kmlem2  10105  kmlem13  10116  axdc4lem  10409  zfac  10414  zfcndun  10570  zfcndac  10574  sup2  12145  supmul  12161  climmo  15567  summo  15727  prodmo  15949  gsumval3eu  19927  elpt  23612  gsumwrd2dccatlem  33218  1arithidomlem1  33692  1arithidom  33694  bnj1185  35052  axprALT2  35369  fineqvac  35376  axreg  35387  axregscl  35388  tz9.1regs  35394  satf0op  35691  sat1el2xp  35693  cbvrexvw2  36551  cbvoprab1vw  36561  cbvoprab2vw  36562  cbvoprab13vw  36565  mh-regprimbi  36869  bj-bm1.3ii  37513  wl-ax12v2cl  37964  wl-dfclel  37973  fdc  38208  sn-sup2  43077  cpcoll2d  44799  axc11next  44946  fnchoice  45573  ichexmpl1  48039