Theorem cbvexvw 2032

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774

This theorem is referenced by:  cbvex2vw  2036  mojust  2525  mo4  2552  eujust  2557  cbveuvw  2592  clelab  2871  cbvrexvw  3227  cbvrexdva2OLD  3338  euind  3713  reuind  3742  cbvopab1v  5218  cbvopab2v  5220  bm1.3ii  5293  reusv2lem2  5388  relop  5841  dmcoss  5961  fv3  6900  exfo  7097  zfun  7720  suppimacnv  8154  frrlem1  8267  wfrlem1OLD  8304  ac6sfi  9284  brwdom2  9565  ttrclss  9712  ttrclselem2  9718  aceq1  10109  aceq0  10110  aceq3lem  10112  dfac4  10114  kmlem2  10143  kmlem13  10154  axdc4lem  10447  zfac  10452  zfcndun  10607  zfcndac  10611  sup2  12168  supmul  12184  climmo  15499  summo  15661  prodmo  15878  gsumval3eu  19816  elpt  23400  bnj1185  34295  fineqvac  34588  satf0op  34859  sat1el2xp  34861  bj-bm1.3ii  36436  fdc  37107  sn-sup2  41856  cpcoll2d  43532  axc11next  43679  fnchoice  44227  ichexmpl1  46647