Theorem cbvexvw 2041

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2402 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 1537  ∃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 397  df-ex 1783

This theorem is referenced by:  cbvex2vw  2045  mojust  2540  mo4  2567  eujust  2572  cbveuvw  2607  clelab  2884  cbvrexvw  3385  cbvrexdva2  3394  euind  3660  reuind  3689  cbvopab1v  5154  cbvopab2v  5156  bm1.3ii  5227  reusv2lem2  5323  relop  5762  dmcoss  5883  fv3  6801  exfo  6990  zfun  7598  suppimacnv  7999  frrlem1  8111  wfrlem1OLD  8148  ac6sfi  9067  brwdom2  9341  ttrclss  9487  ttrclselem2  9493  aceq1  9882  aceq0  9883  aceq3lem  9885  dfac4  9887  kmlem2  9916  kmlem13  9927  axdc4lem  10220  zfac  10225  zfcndun  10380  zfcndac  10384  sup2  11940  supmul  11956  climmo  15275  summo  15438  prodmo  15655  gsumval3eu  19514  elpt  22732  bnj1185  32782  fineqvac  33075  satf0op  33348  sat1el2xp  33350  bj-bm1.3ii  35244  fdc  35912  sn-sup2  40446  cpcoll2d  41884  axc11next  42031  fnchoice  42579  ichexmpl1  44932