Theorem df1o2 8412

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

Syntax hints:   = wceq 1542  ∅c0 4273  {csn 4567  suc csuc 6325  1_oc1o 8398

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-un 3894  df-nul 4274  df-suc 6329  df-1o 8405

This theorem is referenced by:  df2o3  8413  df2o2  8414  1oex  8415  1n0  8423  nlim1  8424  el1o  8430  dif1o  8435  0we1  8441  oeeui  8538  map0e  8830  ensn1  8968  en1  8971  map1  8987  xp1en  9001  0sdom1dom  9156  1sdom2  9158  sdom1  9160  1sdom2dom  9164  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  14332  sylow2alem2  19593  psr1baslem  22148  fvcoe1  22171  coe1f2  22173  coe1sfi  22177  coe1add  22229  coe1mul2lem1  22232  coe1mul2lem2  22233  coe1mul2  22234  coe1tm  22238  ply1coe  22263  evls1rhmlem  22286  evl1sca  22299  evl1var  22301  pf1mpf  22317  pf1ind  22320  mat0dimbas0  22431  mavmul0g  22518  hmph0  23760  tdeglem2  26026  deg1ldg  26057  deg1leb  26060  deg1val  26061  old1  27857  fply1  33618  bnj105  34867  bnj96  35007  bnj98  35009  bnj149  35017  r11  35237  r12  35238  fineqvnttrclselem1  35265  rankeq1o  36353  ordcmp  36629  ssoninhaus  36630  onint1  36631  poimirlem28  37969  reheibor  38160  wopprc  43458  pwslnmlem0  43519  pwfi2f1o  43524  nadd1suc  43820  lincval0  48891  lco0  48903  linds0  48941  f1omo  49368  setc1oterm  49966  setc1ohomfval  49968  setc1ocofval  49969  funcsetc1o  49972  isinito2lem  49973  setc1onsubc  50077