Theorem cbvexvw 2070

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  cbvex2vw  2074  mojust  2565  mo4  2593  eujust  2598  cbveuvw  2632  iseqsetvlem  2825  cbvrexvw  3243  euind  3685  reuind  3714  cbvopab1v  5187  cbvopab2v  5188  bm1.3iiOLD  5263  reusv2lem2  5368  axprg  5406  relop  5834  dmcoss  5963  dmcossOLD  5964  fv3  6900  exfo  7102  cbvoprab3v  7509  zfun  7741  suppimacnv  8176  frrlem1  8289  ac6sfi  9258  brwdom2  9549  ttrclss  9703  ttrclselem2  9709  aceq1  10124  aceq0  10125  aceq3lem  10127  dfac4  10129  kmlem2  10158  kmlem13  10169  axdc4lem  10461  zfac  10466  zfcndun  10628  zfcndac  10632  sup2  12199  supmul  12215  climmo  15648  summo  15807  prodmo  16029  gsumval3eu  20037  elpt  23804  gsumwrd2dccatlem  33525  1arithidomlem1  33953  1arithidom  33955  bnj1185  35310  axprALT2  35625  fineqvac  35650  axreg  35661  axregscl  35662  tz9.1regs  35668  satf0op  35964  sat1el2xp  35966  cbvrexvw2  36855  cbvoprab1vw  36865  cbvoprab2vw  36866  cbvoprab13vw  36869  mh-regprimbi  37172  bj-bm1.3ii  37816  wl-ax12v2cl  38268  wl-dfclel  38277  fdc  38503  sn-sup2  43387  cpcoll2d  45091  axc11next  45238  fnchoice  45871  ichexmpl1  48377  cbvals  50742