Theorem df1o2 8402

Description: Expanded value of the ordinal number 1. Definition 2.1 of [Schloeder] p. 4. (Contributed by NM, 4-Nov-2002.)

Assertion

Ref	Expression
df1o2	⊢ 1o = {∅}

Proof of Theorem df1o2

Step	Hyp	Ref	Expression
1		df-1o 8395	. 2 ⊢ 1o = suc ∅
2		suc0 6392	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2757	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1541  ∅c0 4283  {csn 4578  suc csuc 6317  1_oc1o 8388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902  df-un 3904  df-nul 4284  df-suc 6321  df-1o 8395

This theorem is referenced by:  df2o3  8403  df2o2  8404  1oex  8405  1n0  8413  nlim1  8414  el1o  8420  dif1o  8425  0we1  8431  oeeui  8528  map0e  8818  ensn1  8956  en1  8959  map1  8975  xp1en  8989  0sdom1dom  9144  1sdom2  9146  sdom1  9148  1sdom2dom  9152  ssttrcl  9622  ttrclss  9627  ttrclselem2  9633  infxpenlem  9921  fseqenlem1  9932  dju1dif  10081  infdju1  10098  pwdju1  10099  infmap2  10125  cflim2  10171  pwxpndom2  10574  pwdjundom  10576  gchxpidm  10578  wuncval2  10656  tsk1  10673  hashen1  14291  sylow2alem2  19545  psr1baslem  22123  fvcoe1  22146  coe1f2  22148  coe1sfi  22152  coe1add  22204  coe1mul2lem1  22207  coe1mul2lem2  22208  coe1mul2  22209  coe1tm  22213  ply1coe  22240  evls1rhmlem  22263  evl1sca  22276  evl1var  22278  pf1mpf  22294  pf1ind  22297  mat0dimbas0  22408  mavmul0g  22495  hmph0  23737  tdeglem2  26020  deg1ldg  26051  deg1leb  26054  deg1val  26055  old1  27847  fply1  33588  bnj105  34829  bnj96  34970  bnj98  34972  bnj149  34980  r11  35199  r12  35200  fineqvnttrclselem1  35226  rankeq1o  36314  ordcmp  36590  ssoninhaus  36591  onint1  36592  poimirlem28  37788  reheibor  37979  wopprc  43214  pwslnmlem0  43275  pwfi2f1o  43280  nadd1suc  43576  lincval0  48603  lco0  48615  linds0  48653  f1omo  49080  setc1oterm  49678  setc1ohomfval  49680  setc1ocofval  49681  funcsetc1o  49684  isinito2lem  49685  setc1onsubc  49789