Theorem df1o2 8403

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 8396	. 2 ⊢ 1o = suc ∅
2		suc0 6388	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2762	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1547  ∅c0 4262  {csn 4556  suc csuc 6313  1_oc1o 8389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-un 3888  df-nul 4263  df-suc 6317  df-1o 8396

This theorem is referenced by:  df2o3  8404  df2o2  8405  1oex  8406  1n0  8414  nlim1  8415  el1o  8421  dif1o  8426  0we1  8432  oeeui  8529  map0e  8821  ensn1  8959  en1  8962  map1  8978  xp1en  8992  0sdom1dom  9147  1sdom2  9149  sdom1  9151  1sdom2dom  9155  ssttrcl  9628  ttrclss  9633  ttrclselem2  9639  infxpenlem  9927  fseqenlem1  9938  dju1dif  10087  infdju1  10104  pwdju1  10105  infmap2  10131  cflim2  10177  pwxpndom2  10580  pwdjundom  10582  gchxpidm  10584  wuncval2  10662  tsk1  10679  hashen1  14324  sylow2alem2  19585  psr1baslem  22171  fvcoe1  22193  coe1f2  22195  coe1sfi  22199  coe1add  22251  coe1mul2lem1  22254  coe1mul2lem2  22255  coe1mul2  22256  coe1tm  22260  ply1coe  22285  evls1rhmlem  22308  evl1sca  22321  evl1var  22323  pf1mpf  22339  pf1ind  22342  mat0dimbas0  22450  mavmul0g  22537  hmph0  23779  tdeglem2  26045  deg1ldg  26076  deg1leb  26079  deg1val  26080  old1  27876  fply1  33650  selvply1rhmlema  33711  selvply1rhmlemb  33712  selvply1rhmlem1  33713  selvply1rhm0  33719  bnj105  34916  bnj96  35056  bnj98  35058  bnj149  35066  r11  35284  r12  35285  fineqvnttrclselem1  35311  rankeq1o  36408  ordcmp  36684  ssoninhaus  36685  onint1  36686  poimirlem28  38024  reheibor  38215  wopprc  43484  pwslnmlem0  43545  pwfi2f1o  43550  nadd1suc  43846  lincval0  48914  lco0  48926  linds0  48964  f1omo  49391  setc1oterm  49989  setc1ohomfval  49991  setc1ocofval  49992  funcsetc1o  49995  isinito2lem  49996  setc1onsubc  50100