Theorem df1o2 8450

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

Syntax hints:   = wceq 1540  ∅c0 4304  {csn 4597  suc csuc 6342  1_oc1o 8436

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 3457  df-dif 3925  df-un 3927  df-nul 4305  df-suc 6346  df-1o 8443

This theorem is referenced by:  df2o3  8451  df2o2  8452  1oex  8453  1n0  8463  nlim1  8464  el1o  8470  dif1o  8475  0we1  8481  oeeui  8577  map0e  8859  ensn1  8998  en1  9001  map1  9017  xp1en  9034  0sdom1dom  9203  1sdom2  9205  sdom1  9207  1sdom2dom  9212  ssttrcl  9686  ttrclss  9691  ttrclselem2  9697  infxpenlem  9984  fseqenlem1  9995  dju1dif  10144  infdju1  10161  pwdju1  10162  infmap2  10188  cflim2  10234  pwxpndom2  10636  pwdjundom  10638  gchxpidm  10640  wuncval2  10718  tsk1  10735  hashen1  14345  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  25973  deg1ldg  26004  deg1leb  26007  deg1val  26008  old1  27794  fply1  33535  bnj105  34722  bnj96  34863  bnj98  34865  bnj149  34873  rankeq1o  36156  ordcmp  36432  ssoninhaus  36433  onint1  36434  poimirlem28  37639  reheibor  37830  wopprc  42991  pwslnmlem0  43052  pwfi2f1o  43057  nadd1suc  43353  lincval0  48333  lco0  48345  linds0  48383  setc1oterm  49369  setc1ohomfval  49371  setc1ocofval  49372  funcsetc1o  49375  isinito2lem  49376  setc1onsubc  49480