Theorem df1o2 8404

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 8397	. 2 ⊢ 1o = suc ∅
2		suc0 6394	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2759	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1541  ∅c0 4285  {csn 4580  suc csuc 6319  1_oc1o 8390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-un 3906  df-nul 4286  df-suc 6323  df-1o 8397

This theorem is referenced by:  df2o3  8405  df2o2  8406  1oex  8407  1n0  8415  nlim1  8416  el1o  8422  dif1o  8427  0we1  8433  oeeui  8530  map0e  8822  ensn1  8960  en1  8963  map1  8979  xp1en  8993  0sdom1dom  9148  1sdom2  9150  sdom1  9152  1sdom2dom  9156  ssttrcl  9626  ttrclss  9631  ttrclselem2  9637  infxpenlem  9925  fseqenlem1  9936  dju1dif  10085  infdju1  10102  pwdju1  10103  infmap2  10129  cflim2  10175  pwxpndom2  10578  pwdjundom  10580  gchxpidm  10582  wuncval2  10660  tsk1  10677  hashen1  14295  sylow2alem2  19549  psr1baslem  22127  fvcoe1  22150  coe1f2  22152  coe1sfi  22156  coe1add  22208  coe1mul2lem1  22211  coe1mul2lem2  22212  coe1mul2  22213  coe1tm  22217  ply1coe  22244  evls1rhmlem  22267  evl1sca  22280  evl1var  22282  pf1mpf  22298  pf1ind  22301  mat0dimbas0  22412  mavmul0g  22499  hmph0  23741  tdeglem2  26024  deg1ldg  26055  deg1leb  26058  deg1val  26059  old1  27863  fply1  33641  bnj105  34882  bnj96  35023  bnj98  35025  bnj149  35033  r11  35252  r12  35253  fineqvnttrclselem1  35279  rankeq1o  36367  ordcmp  36643  ssoninhaus  36644  onint1  36645  poimirlem28  37851  reheibor  38042  wopprc  43293  pwslnmlem0  43354  pwfi2f1o  43359  nadd1suc  43655  lincval0  48682  lco0  48694  linds0  48732  f1omo  49159  setc1oterm  49757  setc1ohomfval  49759  setc1ocofval  49760  funcsetc1o  49763  isinito2lem  49764  setc1onsubc  49868