Theorem df1o2 8443

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 8436	. 2 ⊢ 1o = suc ∅
2		suc0 6411	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2753	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1540  ∅c0 4298  {csn 4591  suc csuc 6336  1_oc1o 8429

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3919  df-un 3921  df-nul 4299  df-suc 6340  df-1o 8436

This theorem is referenced by:  df2o3  8444  df2o2  8445  1oex  8446  1n0  8454  nlim1  8455  el1o  8461  dif1o  8466  0we1  8472  oeeui  8568  map0e  8857  ensn1  8994  en1  8997  map1  9013  xp1en  9030  0sdom1dom  9191  1sdom2  9193  sdom1  9195  1sdom2dom  9200  ssttrcl  9674  ttrclss  9679  ttrclselem2  9685  infxpenlem  9972  fseqenlem1  9983  dju1dif  10132  infdju1  10149  pwdju1  10150  infmap2  10176  cflim2  10222  pwxpndom2  10624  pwdjundom  10626  gchxpidm  10628  wuncval2  10706  tsk1  10723  hashen1  14341  sylow2alem2  19554  psr1baslem  22075  fvcoe1  22098  coe1f2  22100  coe1sfi  22104  coe1add  22156  coe1mul2lem1  22159  coe1mul2lem2  22160  coe1mul2  22161  coe1tm  22165  ply1coe  22191  evls1rhmlem  22214  evl1sca  22227  evl1var  22229  pf1mpf  22245  pf1ind  22248  mat0dimbas0  22359  mavmul0g  22446  hmph0  23688  tdeglem2  25972  deg1ldg  26003  deg1leb  26006  deg1val  26007  old1  27793  fply1  33533  bnj105  34720  bnj96  34861  bnj98  34863  bnj149  34871  rankeq1o  36154  ordcmp  36430  ssoninhaus  36431  onint1  36432  poimirlem28  37637  reheibor  37828  wopprc  43012  pwslnmlem0  43073  pwfi2f1o  43078  nadd1suc  43374  lincval0  48394  lco0  48406  linds0  48444  f1omo  48871  setc1oterm  49470  setc1ohomfval  49472  setc1ocofval  49473  funcsetc1o  49476  isinito2lem  49477  setc1onsubc  49581