Theorem cbvexvw 2041

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012

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

This theorem is referenced by:  cbvex2vw  2045  mojust  2539  mo4  2566  eujust  2571  cbveuvw  2606  clelab  2882  cbvrexvw  3373  cbvrexdva2  3382  euind  3654  reuind  3683  cbvopab1v  5149  cbvopab2v  5151  bm1.3ii  5221  reusv2lem2  5317  relop  5748  dmcoss  5869  fv3  6774  exfo  6963  zfun  7567  suppimacnv  7961  frrlem1  8073  wfrlem1OLD  8110  ac6sfi  8988  brwdom2  9262  aceq1  9804  aceq0  9805  aceq3lem  9807  dfac4  9809  kmlem2  9838  kmlem13  9849  axdc4lem  10142  zfac  10147  zfcndun  10302  zfcndac  10306  sup2  11861  supmul  11877  climmo  15194  summo  15357  prodmo  15574  gsumval3eu  19420  elpt  22631  bnj1185  32673  fineqvac  32966  satf0op  33239  sat1el2xp  33241  ttrclss  33706  ttrclselem2  33712  bj-bm1.3ii  35162  fdc  35830  sn-sup2  40360  cpcoll2d  41766  axc11next  41913  fnchoice  42461  ichexmpl1  44809