Theorem cbvexvw 2060

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803

This theorem is referenced by:  cbvex2vw  2064  mojust  2568  mo4  2596  eujust  2601  cbveuvw  2635  iseqsetvlem  2828  cbvrexvw  3244  euind  3690  reuind  3719  cbvopab1v  5183  cbvopab2v  5184  bm1.3iiOLD  5257  reusv2lem2  5361  axprg  5399  relop  5827  dmcoss  5956  dmcossOLD  5957  fv3  6889  exfo  7090  cbvoprab3v  7492  zfun  7723  suppimacnv  8158  frrlem1  8271  ac6sfi  9232  brwdom2  9523  ttrclss  9677  ttrclselem2  9683  aceq1  10089  aceq0  10090  aceq3lem  10092  dfac4  10094  kmlem2  10123  kmlem13  10134  axdc4lem  10427  zfac  10432  zfcndun  10588  zfcndac  10592  sup2  12162  supmul  12178  climmo  15598  summo  15758  prodmo  15980  gsumval3eu  19965  elpt  23690  gsumwrd2dccatlem  33310  1arithidomlem1  33742  1arithidom  33744  bnj1185  35098  axprALT2  35417  fineqvac  35424  axreg  35435  axregscl  35436  tz9.1regs  35442  satf0op  35740  sat1el2xp  35742  cbvrexvw2  36600  cbvoprab1vw  36610  cbvoprab2vw  36611  cbvoprab13vw  36614  mh-regprimbi  36918  bj-bm1.3ii  37561  wl-ax12v2cl  38012  wl-dfclel  38021  fdc  38256  sn-sup2  43125  cpcoll2d  44833  axc11next  44980  fnchoice  45607  ichexmpl1  48073