Theorem df1o2 8525

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 8518	. 2 ⊢ 1o = suc ∅
2		suc0 6469	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2762	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1537  ∅c0 4347  {csn 4648  suc csuc 6396  1_oc1o 8511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3484  df-dif 3973  df-un 3975  df-nul 4348  df-suc 6400  df-1o 8518

This theorem is referenced by:  df2o3  8526  df2o2  8527  1oex  8528  1n0  8540  nlim1  8541  el1o  8547  dif1o  8552  0we1  8558  oeeui  8654  map0e  8936  ensn1  9078  ensn1OLD  9079  en1  9082  en1OLD  9083  map1  9101  xp1en  9119  0sdom1dom  9297  1sdom2  9299  sdom1  9301  1sdom2dom  9306  pwfiOLD  9413  ssttrcl  9780  ttrclss  9785  ttrclselem2  9791  infxpenlem  10078  fseqenlem1  10089  dju1dif  10238  infdju1  10255  pwdju1  10256  infmap2  10282  cflim2  10328  pwxpndom2  10730  pwdjundom  10732  gchxpidm  10734  wuncval2  10812  tsk1  10829  hashen1  14415  sylow2alem2  19655  psr1baslem  22200  fvcoe1  22223  coe1f2  22225  coe1sfi  22229  coe1add  22281  coe1mul2lem1  22284  coe1mul2lem2  22285  coe1mul2  22286  coe1tm  22290  ply1coe  22316  evls1rhmlem  22339  evl1sca  22352  evl1var  22354  pf1mpf  22370  pf1ind  22373  mat0dimbas0  22486  mavmul0g  22573  hmph0  23817  tdeglem2  26112  deg1ldg  26143  deg1leb  26146  deg1val  26147  old1  27923  fply1  33541  bnj105  34692  bnj96  34833  bnj98  34835  bnj149  34843  rankeq1o  36127  ordcmp  36360  ssoninhaus  36361  onint1  36362  poimirlem28  37556  reheibor  37747  wopprc  42924  pwslnmlem0  42988  pwfi2f1o  42993  nadd1suc  43294  lincval0  48062  lco0  48074  linds0  48112