Theorem cbvexvw 2040

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1539  ∃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 1913  ax-6 1971  ax-7 2011

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  cbvex2vw  2044  mojust  2533  mo4  2560  eujust  2565  cbveuvw  2600  clelab  2879  cbvrexvw  3235  cbvrexdva2OLD  3346  euind  3720  reuind  3749  cbvopab1v  5227  cbvopab2v  5229  bm1.3ii  5302  reusv2lem2  5397  relop  5850  dmcoss  5970  fv3  6909  exfo  7106  zfun  7728  suppimacnv  8161  frrlem1  8273  wfrlem1OLD  8310  ac6sfi  9289  brwdom2  9570  ttrclss  9717  ttrclselem2  9723  aceq1  10114  aceq0  10115  aceq3lem  10117  dfac4  10119  kmlem2  10148  kmlem13  10159  axdc4lem  10452  zfac  10457  zfcndun  10612  zfcndac  10616  sup2  12174  supmul  12190  climmo  15505  summo  15667  prodmo  15884  gsumval3eu  19813  elpt  23296  bnj1185  34090  fineqvac  34383  satf0op  34654  sat1el2xp  34656  bj-bm1.3ii  36248  fdc  36916  sn-sup2  41644  cpcoll2d  43320  axc11next  43467  fnchoice  44015  ichexmpl1  46436