Theorem df1o2 8418

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

Syntax hints:   = wceq 1540  ∅c0 4292  {csn 4585  suc csuc 6322  1_oc1o 8404

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 3446  df-dif 3914  df-un 3916  df-nul 4293  df-suc 6326  df-1o 8411

This theorem is referenced by:  df2o3  8419  df2o2  8420  1oex  8421  1n0  8429  nlim1  8430  el1o  8436  dif1o  8441  0we1  8447  oeeui  8543  map0e  8832  ensn1  8969  en1  8972  map1  8988  xp1en  9004  0sdom1dom  9162  1sdom2  9164  sdom1  9166  1sdom2dom  9170  ssttrcl  9644  ttrclss  9649  ttrclselem2  9655  infxpenlem  9942  fseqenlem1  9953  dju1dif  10102  infdju1  10119  pwdju1  10120  infmap2  10146  cflim2  10192  pwxpndom2  10594  pwdjundom  10596  gchxpidm  10598  wuncval2  10676  tsk1  10693  hashen1  14311  sylow2alem2  19532  psr1baslem  22102  fvcoe1  22125  coe1f2  22127  coe1sfi  22131  coe1add  22183  coe1mul2lem1  22186  coe1mul2lem2  22187  coe1mul2  22188  coe1tm  22192  ply1coe  22218  evls1rhmlem  22241  evl1sca  22254  evl1var  22256  pf1mpf  22272  pf1ind  22275  mat0dimbas0  22386  mavmul0g  22473  hmph0  23715  tdeglem2  25999  deg1ldg  26030  deg1leb  26033  deg1val  26034  old1  27824  fply1  33520  bnj105  34707  bnj96  34848  bnj98  34850  bnj149  34858  rankeq1o  36152  ordcmp  36428  ssoninhaus  36429  onint1  36430  poimirlem28  37635  reheibor  37826  wopprc  43012  pwslnmlem0  43073  pwfi2f1o  43078  nadd1suc  43374  lincval0  48397  lco0  48409  linds0  48447  f1omo  48874  setc1oterm  49473  setc1ohomfval  49475  setc1ocofval  49476  funcsetc1o  49479  isinito2lem  49480  setc1onsubc  49584