Theorem cbvexvw 2072

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 2071	. . 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 1945  ax-6 2002  ax-7 2043

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

This theorem is used by:  cbvex2vw  2076  mojust  2566  mo4  2594  eujust  2599  cbveuvw  2633  iseqsetvlem  2826  cbvrexvw  3245  euind  3685  reuind  3714  cbvopab1v  5186  cbvopab2v  5187  reusv2lem2  5365  axprg  5399  relop  5834  dmcoss  5964  dmcossOLD  5965  fv3  6926  exfo  7129  cbvoprab3v  7535  zfun  7776  suppimacnv  8219  frrlem1  8332  ac6sfi  9303  brwdom2  9594  ttrclss  9748  ttrclselem2  9754  aceq1  10223  aceq0  10224  aceq3lem  10226  dfac4  10228  kmlem2  10257  kmlem13  10268  axdc4lem  10560  zfac  10565  zfcndun  10727  zfcndac  10731  sup2  12300  supmul  12316  climmo  15753  summo  15912  prodmo  16132  gsumval3eu  20148  elpt  23921  gsumwrd2dccatlem  33708  1arithidomlem1  34137  1arithidom  34139  bnj1185  35493  rmo6  35780  axprALT2  35816  fineqvac  35884  axreg  35895  axregscl  35896  tz9.1regs  35902  satf0op  36309  sat1el2xp  36311  mirimanoffr  36627  cbvrexvw2  37194  cbvoprab1vw  37204  cbvoprab2vw  37205  cbvoprab13vw  37208  mh-regprimbi  37511  bj-bm1.3ii  38170  wl-ax12v2cl  38621  wl-dfclel  38630  fdc  38871  sn-sup2  43748  cpcoll2d  45435  axc11next  45582  fnchoice  46251  ichexmpl1  48756  cbvals  51181