Theorem cbvexvw 2038

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1539  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by:  cbvex2vw  2042  mojust  2538  mo4  2566  eujust  2571  cbveuvw  2605  iseqsetvlem  2799  cbvrexvw  3215  euind  3682  reuind  3711  cbvopab1v  5176  cbvopab2v  5177  bm1.3iiOLD  5247  reusv2lem2  5344  relop  5799  dmcoss  5924  dmcossOLD  5925  fv3  6852  exfo  7050  cbvoprab3v  7450  zfun  7681  suppimacnv  8116  frrlem1  8228  ac6sfi  9184  brwdom2  9478  ttrclss  9629  ttrclselem2  9635  aceq1  10027  aceq0  10028  aceq3lem  10030  dfac4  10032  kmlem2  10062  kmlem13  10073  axdc4lem  10365  zfac  10370  zfcndun  10526  zfcndac  10530  sup2  12098  supmul  12114  climmo  15480  summo  15640  prodmo  15859  gsumval3eu  19833  elpt  23516  gsumwrd2dccatlem  33159  1arithidomlem1  33616  1arithidom  33618  bnj1185  34949  fineqvac  35272  axreg  35283  axregscl  35284  tz9.1regs  35290  satf0op  35571  sat1el2xp  35573  cbvrexvw2  36421  cbvoprab1vw  36431  cbvoprab2vw  36432  cbvoprab13vw  36435  bj-bm1.3ii  37265  wl-ax12v2cl  37707  fdc  37942  sn-sup2  42742  cpcoll2d  44496  axc11next  44643  fnchoice  45270  ichexmpl1  47711