Theorem df1o2 8398

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 8391	. 2 ⊢ 1o = suc ∅
2		suc0 6389	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2754	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1541  ∅c0 4282  {csn 4575  suc csuc 6314  1_oc1o 8384

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-un 3902  df-nul 4283  df-suc 6318  df-1o 8391

This theorem is referenced by:  df2o3  8399  df2o2  8400  1oex  8401  1n0  8409  nlim1  8410  el1o  8416  dif1o  8421  0we1  8427  oeeui  8523  map0e  8812  ensn1  8949  en1  8952  map1  8968  xp1en  8982  0sdom1dom  9136  1sdom2  9138  sdom1  9140  1sdom2dom  9144  ssttrcl  9611  ttrclss  9616  ttrclselem2  9622  infxpenlem  9910  fseqenlem1  9921  dju1dif  10070  infdju1  10087  pwdju1  10088  infmap2  10114  cflim2  10160  pwxpndom2  10562  pwdjundom  10564  gchxpidm  10566  wuncval2  10644  tsk1  10661  hashen1  14283  sylow2alem2  19536  psr1baslem  22103  fvcoe1  22126  coe1f2  22128  coe1sfi  22132  coe1add  22184  coe1mul2lem1  22187  coe1mul2lem2  22188  coe1mul2  22189  coe1tm  22193  ply1coe  22219  evls1rhmlem  22242  evl1sca  22255  evl1var  22257  pf1mpf  22273  pf1ind  22276  mat0dimbas0  22387  mavmul0g  22474  hmph0  23716  tdeglem2  25999  deg1ldg  26030  deg1leb  26033  deg1val  26034  old1  27826  fply1  33528  bnj105  34743  bnj96  34884  bnj98  34886  bnj149  34894  r11  35112  r12  35113  fineqvnttrclselem1  35148  rankeq1o  36222  ordcmp  36498  ssoninhaus  36499  onint1  36500  poimirlem28  37694  reheibor  37885  wopprc  43128  pwslnmlem0  43189  pwfi2f1o  43194  nadd1suc  43490  lincval0  48521  lco0  48533  linds0  48571  f1omo  48998  setc1oterm  49597  setc1ohomfval  49599  setc1ocofval  49600  funcsetc1o  49603  isinito2lem  49604  setc1onsubc  49708