Theorem df1o2 8414

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 8407	. 2 ⊢ 1o = suc ∅
2		suc0 6402	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2760	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1542  ∅c0 4287  {csn 4582  suc csuc 6327  1_oc1o 8400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-un 3908  df-nul 4288  df-suc 6331  df-1o 8407

This theorem is referenced by:  df2o3  8415  df2o2  8416  1oex  8417  1n0  8425  nlim1  8426  el1o  8432  dif1o  8437  0we1  8443  oeeui  8540  map0e  8832  ensn1  8970  en1  8973  map1  8989  xp1en  9003  0sdom1dom  9158  1sdom2  9160  sdom1  9162  1sdom2dom  9166  ssttrcl  9636  ttrclss  9641  ttrclselem2  9647  infxpenlem  9935  fseqenlem1  9946  dju1dif  10095  infdju1  10112  pwdju1  10113  infmap2  10139  cflim2  10185  pwxpndom2  10588  pwdjundom  10590  gchxpidm  10592  wuncval2  10670  tsk1  10687  hashen1  14305  sylow2alem2  19562  psr1baslem  22140  fvcoe1  22163  coe1f2  22165  coe1sfi  22169  coe1add  22221  coe1mul2lem1  22224  coe1mul2lem2  22225  coe1mul2  22226  coe1tm  22230  ply1coe  22257  evls1rhmlem  22280  evl1sca  22293  evl1var  22295  pf1mpf  22311  pf1ind  22314  mat0dimbas0  22425  mavmul0g  22512  hmph0  23754  tdeglem2  26037  deg1ldg  26068  deg1leb  26071  deg1val  26072  old1  27876  fply1  33655  bnj105  34905  bnj96  35045  bnj98  35047  bnj149  35055  r11  35275  r12  35276  fineqvnttrclselem1  35303  rankeq1o  36391  ordcmp  36667  ssoninhaus  36668  onint1  36669  poimirlem28  37903  reheibor  38094  wopprc  43391  pwslnmlem0  43452  pwfi2f1o  43457  nadd1suc  43753  lincval0  48779  lco0  48791  linds0  48829  f1omo  49256  setc1oterm  49854  setc1ohomfval  49856  setc1ocofval  49857  funcsetc1o  49860  isinito2lem  49861  setc1onsubc  49965