Theorem cbvexvw 2040

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777

This theorem is referenced by:  cbvex2vw  2044  mojust  2617  mo4  2646  eujust  2652  cbvrexvw  3450  cbvrexdva2  3457  elisset  3505  euind  3714  reuind  3743  cbvopab2v  5136  bm1.3ii  5198  reusv2lem2  5291  relop  5715  dmcoss  5836  fv3  6682  exfo  6865  zfun  7456  suppimacnv  7835  wfrlem1  7948  ac6sfi  8756  brwdom2  9031  aceq1  9537  aceq0  9538  aceq3lem  9540  dfac4  9542  kmlem2  9571  kmlem13  9582  axdc4lem  9871  zfac  9876  zfcndun  10031  zfcndac  10035  sup2  11591  supmul  11607  climmo  14908  summo  15068  prodmo  15284  gsumval3eu  19018  elpt  22174  bnj1185  32060  satf0op  32619  sat1el2xp  32621  frrlem1  33118  bj-bm1.3ii  34351  fdc  35014  cpcoll2d  40588  axc11next  40731  fnchoice  41279  ichexmpl1  43625