Theorem cbvexvw 2044

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207  ∀wal 1545  ∃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 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  cbvex2vw  2048  mojust  2542  mo4  2570  eujust  2575  cbveuvw  2609  iseqsetvlem  2803  cbvrexvw  3219  euind  3672  reuind  3701  cbvopab1v  5157  cbvopab2v  5158  bm1.3iiOLD  5231  reusv2lem2  5335  axprg  5373  relop  5799  dmcoss  5924  dmcossOLD  5925  fv3  6852  exfo  7053  cbvoprab3v  7455  zfun  7686  suppimacnv  8121  frrlem1  8233  ac6sfi  9191  brwdom2  9485  ttrclss  9639  ttrclselem2  9645  aceq1  10037  aceq0  10038  aceq3lem  10040  dfac4  10042  kmlem2  10072  kmlem13  10083  axdc4lem  10375  zfac  10380  zfcndun  10536  zfcndac  10540  sup2  12110  supmul  12126  climmo  15517  summo  15677  prodmo  15899  gsumval3eu  19877  elpt  23562  gsumwrd2dccatlem  33165  1arithidomlem1  33625  1arithidom  33627  bnj1185  34982  axprALT2  35297  fineqvac  35304  axreg  35315  axregscl  35316  tz9.1regs  35322  satf0op  35612  sat1el2xp  35614  cbvrexvw2  36462  cbvoprab1vw  36472  cbvoprab2vw  36473  cbvoprab13vw  36476  mh-regprimbi  36780  bj-bm1.3ii  37424  wl-ax12v2cl  37875  wl-dfclel  37884  fdc  38119  sn-sup2  42988  cpcoll2d  44710  axc11next  44857  fnchoice  45484  ichexmpl1  47951