Theorem cbvexvw 2049

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 321	. . . 4 ⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜓))
3	2	cbvalvw 2048	. . 3 ⊢ (∀𝑥 ¬ 𝜑 ↔ ∀𝑦 ¬ 𝜓)
4	3	notbii 323	. 2 ⊢ (¬ ∀𝑥 ¬ 𝜑 ↔ ¬ ∀𝑦 ¬ 𝜓)
5		df-ex 1787	. 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
6		df-ex 1787	. 2 ⊢ (∃𝑦𝜓 ↔ ¬ ∀𝑦 ¬ 𝜓)
7	4, 5, 6	3bitr4i 306	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1540  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787

This theorem is referenced by:  cbvex2vw  2053  mojust  2539  mo4  2566  eujust  2572  cbveuvw  2607  clelab  2875  cbvrexvw  3350  cbvrexdva2  3359  euind  3623  reuind  3652  cbvopab2v  5108  bm1.3ii  5170  reusv2lem2  5266  relop  5693  dmcoss  5814  fv3  6694  exfo  6883  zfun  7482  suppimacnv  7871  wfrlem1  7985  ac6sfi  8838  brwdom2  9112  aceq1  9619  aceq0  9620  aceq3lem  9622  dfac4  9624  kmlem2  9653  kmlem13  9664  axdc4lem  9957  zfac  9962  zfcndun  10117  zfcndac  10121  sup2  11676  supmul  11692  climmo  15006  summo  15169  prodmo  15384  gsumval3eu  19145  elpt  22325  bnj1185  32346  fineqvac  32639  satf0op  32912  sat1el2xp  32914  frrlem1  33445  bj-bm1.3ii  34880  fdc  35548  sn-sup2  40038  cpcoll2d  41441  axc11next  41584  fnchoice  42132  ichexmpl1  44484