Theorem df1o2 8465

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 8458	. 2 ⊢ 1o = suc ∅
2		suc0 6435	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2783	1 ⊢ 1o = {∅}

This proof depends on syntax axioms:   = wceq 1570  ∅c0 4279  {csn 4584  suc csuc 6359  1_oc1o 8451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-un 3904  df-nul 4280  df-suc 6363  df-1o 8458

This theorem is used by:  df2o3  8466  df2o2  8467  1oex  8468  1n0OLD  8478  nlim1  8479  el1o  8485  dif1o  8490  0we1  8496  oeeui  8593  map0e  8892  ensn1  9030  en1  9033  map1  9050  xp1en  9064  0sdom1dom  9219  1sdom2  9221  sdom1  9223  1sdom2dom  9227  ssttrcl  9697  ttrclss  9702  ttrclselem2  9708  infxpenlem  10019  fseqenlem1  10030  dju1dif  10178  infdju1  10195  pwdju1  10196  infmap2  10222  cflim2  10268  pwxpndom2  10677  pwdjundom  10679  gchxpidm  10681  wuncval2  10759  tsk1  10776  hashen1  14437  sylow2alem2  19748  psr1baslem  22413  fvcoe1  22435  coe1f2  22437  coe1sfi  22441  coe1add  22493  coe1mul2lem1  22496  coe1mul2lem2  22497  coe1mul2  22498  coe1tm  22502  ply1coe  22526  evls1rhmlem  22549  evl1sca  22562  evl1var  22564  pf1mpf  22580  pf1ind  22583  mat0dimbas0  22691  mavmul0g  22778  hmph0  24024  tdeglem2  26289  deg1ldg  26320  deg1leb  26323  deg1val  26324  old1  28133  fply1  33971  selvply1rhmlema  34031  selvply1rhmlemb  34032  selvply1rhmlem1  34033  selvply1rhm0  34039  bnj105  35237  bnj96  35377  bnj98  35379  bnj149  35387  r11  35604  r12  35605  fineqvnttrclselem1  35650  rankeq1o  36754  nmulrid  36780  ordcmp  37069  ssoninhaus  37070  onint1  37071  poimirlem28  38400  reheibor  38592  wopprc  43874  pwslnmlem0  43935  pwfi2f1o  43940  nadd1suc  44236  lincval0  49348  lco0  49360  linds0  49398  f1omo  49822  setc1oterm  50420  setc1ohomfval  50422  setc1ocofval  50423  funcsetc1o  50426  isinito2lem  50427  setc1onsubc  50531