Theorem df1o2 8445

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 8438	. 2 ⊢ 1o = suc ∅
2		suc0 6424	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2786	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1561  ∅c0 4286  {csn 4583  suc csuc 6349  1_oc1o 8431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-un 3910  df-nul 4287  df-suc 6353  df-1o 8438

This theorem is referenced by:  df2o3  8446  df2o2  8447  1oex  8448  1n0OLD  8458  nlim1  8459  el1o  8465  dif1o  8470  0we1  8476  oeeui  8573  map0e  8865  ensn1  9003  en1  9006  map1  9022  xp1en  9036  0sdom1dom  9191  1sdom2  9193  sdom1  9195  1sdom2dom  9199  ssttrcl  9671  ttrclss  9676  ttrclselem2  9682  infxpenlem  9970  fseqenlem1  9981  dju1dif  10130  infdju1  10147  pwdju1  10148  infmap2  10174  cflim2  10221  pwxpndom2  10624  pwdjundom  10626  gchxpidm  10628  wuncval2  10706  tsk1  10723  hashen1  14384  sylow2alem2  19659  psr1baslem  22248  fvcoe1  22270  coe1f2  22272  coe1sfi  22276  coe1add  22328  coe1mul2lem1  22331  coe1mul2lem2  22332  coe1mul2  22333  coe1tm  22337  ply1coe  22362  evls1rhmlem  22385  evl1sca  22398  evl1var  22400  pf1mpf  22416  pf1ind  22419  mat0dimbas0  22527  mavmul0g  22614  hmph0  23856  tdeglem2  26122  deg1ldg  26153  deg1leb  26156  deg1val  26157  old1  27959  fply1  33755  selvply1rhmlema  33816  selvply1rhmlemb  33817  selvply1rhmlem1  33818  selvply1rhm0  33824  bnj105  35021  bnj96  35161  bnj98  35163  bnj149  35171  r11  35391  r12  35392  fineqvnttrclselem1  35418  rankeq1o  36522  ordcmp  36808  ssoninhaus  36809  onint1  36810  poimirlem28  38148  reheibor  38339  wopprc  43608  pwslnmlem0  43669  pwfi2f1o  43674  nadd1suc  43970  lincval0  49038  lco0  49050  linds0  49088  f1omo  49515  setc1oterm  50113  setc1ohomfval  50115  setc1ocofval  50116  funcsetc1o  50119  isinito2lem  50120  setc1onsubc  50224