Theorem cbvexvw 2139

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198  ∀wal 1651  ∃wex 1875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107

This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876

This theorem is referenced by:  mojust  2590  eujust  2611  euind  3589  reuind  3609  cbvopab2v  4920  bm1.3ii  4978  reusv2lem2  5069  relop  5476  dmcoss  5589  fv3  6429  exfo  6603  zfun  7184  suppimacnv  7543  wfrlem1  7652  ac6sfi  8446  brwdom2  8720  aceq1  9226  aceq0  9227  aceq3lem  9229  dfac4  9231  kmlem2  9261  kmlem13  9272  axdc4lem  9565  zfac  9570  zfcndun  9725  zfcndac  9729  sup2  11271  supmul  11287  climmo  14629  summo  14789  prodmo  15003  gsumval3eu  18620  elpt  21704  bnj1185  31381  frrlem1  32293  bj-denotesv  33349  bj-bm1.3ii  33516  fdc  34028  axc11next  39388  fnchoice  39948