Theorem df1o2 8466

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 8459	. 2 ⊢ 1o = suc ∅
2		suc0 6442	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2788	1 ⊢ 1o = {∅}

This proof depends on syntax axioms:   = wceq 1570  ∅c0 4286  {csn 4591  suc csuc 6366  1_oc1o 8452

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-un 3911  df-nul 4287  df-suc 6370  df-1o 8459

This theorem is used by:  df2o3  8467  df2o2  8468  1oex  8469  1n0OLD  8479  nlim1  8480  el1o  8486  dif1o  8491  0we1  8497  oeeui  8594  map0e  8886  ensn1  9024  en1  9027  map1  9044  xp1en  9058  0sdom1dom  9213  1sdom2  9215  sdom1  9217  1sdom2dom  9221  ssttrcl  9691  ttrclss  9696  ttrclselem2  9702  infxpenlem  10013  fseqenlem1  10024  dju1dif  10172  infdju1  10189  pwdju1  10190  infmap2  10216  cflim2  10262  pwxpndom2  10667  pwdjundom  10669  gchxpidm  10671  wuncval2  10749  tsk1  10766  hashen1  14426  sylow2alem2  19734  psr1baslem  22397  fvcoe1  22419  coe1f2  22421  coe1sfi  22425  coe1add  22477  coe1mul2lem1  22480  coe1mul2lem2  22481  coe1mul2  22482  coe1tm  22486  ply1coe  22510  evls1rhmlem  22533  evl1sca  22546  evl1var  22548  pf1mpf  22564  pf1ind  22567  mat0dimbas0  22675  mavmul0g  22762  hmph0  24005  tdeglem2  26271  deg1ldg  26302  deg1leb  26305  deg1val  26306  old1  28111  fply1  33914  selvply1rhmlema  33974  selvply1rhmlemb  33975  selvply1rhmlem1  33976  selvply1rhm0  33982  bnj105  35180  bnj96  35320  bnj98  35322  bnj149  35330  r11  35547  r12  35548  fineqvnttrclselem1  35593  rankeq1o  36702  nmulrid  36728  ordcmp  37017  ssoninhaus  37018  onint1  37019  poimirlem28  38358  reheibor  38550  wopprc  43817  pwslnmlem0  43878  pwfi2f1o  43883  nadd1suc  44179  lincval0  49254  lco0  49266  linds0  49304  f1omo  49730  setc1oterm  50328  setc1ohomfval  50330  setc1ocofval  50331  funcsetc1o  50334  isinito2lem  50335  setc1onsubc  50439