Theorem cbvexvw 2038

Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2403 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  2536  mo4  2563  eujust  2568  cbveuvw  2602  iseqsetvlem  2796  cbvrexvw  3212  euind  3679  reuind  3708  cbvopab1v  5171  cbvopab2v  5172  bm1.3iiOLD  5242  reusv2lem2  5339  relop  5794  dmcoss  5918  dmcossOLD  5919  fv3  6846  exfo  7044  cbvoprab3v  7444  zfun  7675  suppimacnv  8110  frrlem1  8222  ac6sfi  9175  brwdom2  9466  ttrclss  9617  ttrclselem2  9623  aceq1  10015  aceq0  10016  aceq3lem  10018  dfac4  10020  kmlem2  10050  kmlem13  10061  axdc4lem  10353  zfac  10358  zfcndun  10513  zfcndac  10517  sup2  12085  supmul  12101  climmo  15466  summo  15626  prodmo  15845  gsumval3eu  19818  elpt  23488  gsumwrd2dccatlem  33053  1arithidomlem1  33507  1arithidom  33509  bnj1185  34826  axreg  35146  axregscl  35147  tz9.1regs  35151  fineqvac  35160  satf0op  35442  sat1el2xp  35444  cbvrexvw2  36292  cbvoprab1vw  36302  cbvoprab2vw  36303  cbvoprab13vw  36306  bj-bm1.3ii  37129  wl-ax12v2cl  37571  fdc  37805  sn-sup2  42609  cpcoll2d  44376  axc11next  44523  fnchoice  45150  ichexmpl1  47593