Theorem cbvexvw 2044

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2408 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 2043	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
4	3	notbii 323	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5		df-ex 1782	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6		df-ex 1782	. 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
7	4, 5, 6	3bitr4i 306	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1536  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782

This theorem is referenced by:  cbvex2vw  2048  mojust  2597  mo4  2625  eujust  2631  cbvrexvw  3397  cbvrexdva2  3404  elisset  3452  euind  3663  reuind  3692  cbvopab2v  5108  bm1.3ii  5170  reusv2lem2  5265  relop  5685  dmcoss  5807  fv3  6663  exfo  6848  zfun  7442  suppimacnv  7824  wfrlem1  7937  ac6sfi  8746  brwdom2  9021  aceq1  9528  aceq0  9529  aceq3lem  9531  dfac4  9533  kmlem2  9562  kmlem13  9573  axdc4lem  9866  zfac  9871  zfcndun  10026  zfcndac  10030  sup2  11584  supmul  11600  climmo  14906  summo  15066  prodmo  15282  gsumval3eu  19017  elpt  22177  bnj1185  32175  satf0op  32737  sat1el2xp  32739  frrlem1  33236  bj-bm1.3ii  34481  fdc  35183  sn-sup2  39594  cpcoll2d  40967  axc11next  41110  fnchoice  41658  ichexmpl1  43986