Theorem cbvexvw 2067

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

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

This theorem is referenced by:  cbvex2vw  2071  mojust  2566  mo4  2594  eujust  2599  cbveuvw  2633  iseqsetvlem  2826  cbvrexvw  3244  euind  3688  reuind  3717  cbvopab1v  5190  cbvopab2v  5191  bm1.3iiOLD  5266  reusv2lem2  5372  axprg  5410  relop  5838  dmcoss  5967  dmcossOLD  5968  fv3  6901  exfo  7102  cbvoprab3v  7504  zfun  7735  suppimacnv  8171  frrlem1  8284  ac6sfi  9245  brwdom2  9536  ttrclss  9690  ttrclselem2  9696  aceq1  10102  aceq0  10103  aceq3lem  10105  dfac4  10107  kmlem2  10136  kmlem13  10147  axdc4lem  10440  zfac  10445  zfcndun  10601  zfcndac  10605  sup2  12172  supmul  12188  climmo  15610  summo  15770  prodmo  15992  gsumval3eu  19975  elpt  23710  gsumwrd2dccatlem  33375  1arithidomlem1  33803  1arithidom  33805  bnj1185  35159  axprALT2  35481  fineqvac  35507  axreg  35518  axregscl  35519  tz9.1regs  35525  satf0op  35847  sat1el2xp  35849  cbvrexvw2  36717  cbvoprab1vw  36727  cbvoprab2vw  36728  cbvoprab13vw  36731  mh-regprimbi  37034  bj-bm1.3ii  37678  wl-ax12v2cl  38130  wl-dfclel  38139  fdc  38374  sn-sup2  43243  cpcoll2d  44949  axc11next  45096  fnchoice  45729  ichexmpl1  48195  cbvals  50560