Theorem df1o2 8395

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 8388	. 2 ⊢ 1o = suc ∅
2		suc0 6384	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2752	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1540  ∅c0 4284  {csn 4577  suc csuc 6309  1_oc1o 8381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906  df-un 3908  df-nul 4285  df-suc 6313  df-1o 8388

This theorem is referenced by:  df2o3  8396  df2o2  8397  1oex  8398  1n0  8406  nlim1  8407  el1o  8413  dif1o  8418  0we1  8424  oeeui  8520  map0e  8809  ensn1  8946  en1  8949  map1  8965  xp1en  8980  0sdom1dom  9135  1sdom2  9137  sdom1  9139  1sdom2dom  9143  ssttrcl  9611  ttrclss  9616  ttrclselem2  9622  infxpenlem  9907  fseqenlem1  9918  dju1dif  10067  infdju1  10084  pwdju1  10085  infmap2  10111  cflim2  10157  pwxpndom2  10559  pwdjundom  10561  gchxpidm  10563  wuncval2  10641  tsk1  10658  hashen1  14277  sylow2alem2  19497  psr1baslem  22067  fvcoe1  22090  coe1f2  22092  coe1sfi  22096  coe1add  22148  coe1mul2lem1  22151  coe1mul2lem2  22152  coe1mul2  22153  coe1tm  22157  ply1coe  22183  evls1rhmlem  22206  evl1sca  22219  evl1var  22221  pf1mpf  22237  pf1ind  22240  mat0dimbas0  22351  mavmul0g  22438  hmph0  23680  tdeglem2  25964  deg1ldg  25995  deg1leb  25998  deg1val  25999  old1  27789  fply1  33494  bnj105  34697  bnj96  34838  bnj98  34840  bnj149  34848  fineqvnttrclselem1  35080  rankeq1o  36155  ordcmp  36431  ssoninhaus  36432  onint1  36433  poimirlem28  37638  reheibor  37829  wopprc  43013  pwslnmlem0  43074  pwfi2f1o  43079  nadd1suc  43375  lincval0  48410  lco0  48422  linds0  48460  f1omo  48887  setc1oterm  49486  setc1ohomfval  49488  setc1ocofval  49489  funcsetc1o  49492  isinito2lem  49493  setc1onsubc  49597