Theorem df1o2 8531

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 8524	. 2 ⊢ 1o = suc ∅
2		suc0 6472	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2768	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1537  ∅c0 4352  {csn 4648  suc csuc 6399  1_oc1o 8517

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 2110  ax-9 2118  ax-ext 2711

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 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-nul 4353  df-suc 6403  df-1o 8524

This theorem is referenced by:  df2o3  8532  df2o2  8533  1oex  8534  1n0  8546  nlim1  8547  el1o  8553  dif1o  8558  0we1  8564  oeeui  8660  map0e  8942  ensn1  9084  ensn1OLD  9085  en1  9088  en1OLD  9089  map1  9107  xp1en  9125  0sdom1dom  9303  1sdom2  9305  sdom1  9307  1sdom2dom  9312  pwfiOLD  9419  ssttrcl  9786  ttrclss  9791  ttrclselem2  9797  infxpenlem  10084  fseqenlem1  10095  dju1dif  10244  infdju1  10261  pwdju1  10262  infmap2  10288  cflim2  10334  pwxpndom2  10736  pwdjundom  10738  gchxpidm  10740  wuncval2  10818  tsk1  10835  hashen1  14421  sylow2alem2  19662  psr1baslem  22209  fvcoe1  22232  coe1f2  22234  coe1sfi  22238  coe1add  22290  coe1mul2lem1  22293  coe1mul2lem2  22294  coe1mul2  22295  coe1tm  22299  ply1coe  22325  evls1rhmlem  22348  evl1sca  22361  evl1var  22363  pf1mpf  22379  pf1ind  22382  mat0dimbas0  22495  mavmul0g  22582  hmph0  23826  tdeglem2  26122  deg1ldg  26153  deg1leb  26156  deg1val  26157  old1  27934  fply1  33551  bnj105  34702  bnj96  34843  bnj98  34845  bnj149  34853  rankeq1o  36137  ordcmp  36415  ssoninhaus  36416  onint1  36417  poimirlem28  37610  reheibor  37801  wopprc  42989  pwslnmlem0  43050  pwfi2f1o  43055  nadd1suc  43356  lincval0  48146  lco0  48158  linds0  48196