Theorem cbvexvw 2041

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1540  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783

This theorem is referenced by:  cbvex2vw  2045  mojust  2534  mo4  2561  eujust  2566  cbveuvw  2601  clelab  2880  cbvrexvw  3236  cbvrexdva2OLD  3347  euind  3721  reuind  3750  cbvopab1v  5228  cbvopab2v  5230  bm1.3ii  5303  reusv2lem2  5398  relop  5851  dmcoss  5971  fv3  6910  exfo  7107  zfun  7726  suppimacnv  8159  frrlem1  8271  wfrlem1OLD  8308  ac6sfi  9287  brwdom2  9568  ttrclss  9715  ttrclselem2  9721  aceq1  10112  aceq0  10113  aceq3lem  10115  dfac4  10117  kmlem2  10146  kmlem13  10157  axdc4lem  10450  zfac  10455  zfcndun  10610  zfcndac  10614  sup2  12170  supmul  12186  climmo  15501  summo  15663  prodmo  15880  gsumval3eu  19772  elpt  23076  bnj1185  33804  fineqvac  34097  satf0op  34368  sat1el2xp  34370  bj-bm1.3ii  35945  fdc  36613  sn-sup2  41342  cpcoll2d  43018  axc11next  43165  fnchoice  43713  ichexmpl1  46137