Theorem df1o2 8456

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 8449	. 2 ⊢ 1o = suc ∅
2		suc0 6438	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2786	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1570  ∅c0 4286  {csn 4589  suc csuc 6362  1_oc1o 8442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-un 3910  df-nul 4287  df-suc 6366  df-1o 8449

This theorem is referenced by:  df2o3  8457  df2o2  8458  1oex  8459  1n0OLD  8469  nlim1  8470  el1o  8476  dif1o  8481  0we1  8487  oeeui  8584  map0e  8876  ensn1  9014  en1  9017  map1  9033  xp1en  9047  0sdom1dom  9202  1sdom2  9204  sdom1  9206  1sdom2dom  9210  ssttrcl  9680  ttrclss  9685  ttrclselem2  9691  infxpenlem  9993  fseqenlem1  10004  dju1dif  10152  infdju1  10169  pwdju1  10170  infmap2  10196  cflim2  10242  pwxpndom2  10645  pwdjundom  10647  gchxpidm  10649  wuncval2  10727  tsk1  10744  hashen1  14402  sylow2alem2  19683  psr1baslem  22345  fvcoe1  22367  coe1f2  22369  coe1sfi  22373  coe1add  22425  coe1mul2lem1  22428  coe1mul2lem2  22429  coe1mul2  22430  coe1tm  22434  ply1coe  22458  evls1rhmlem  22481  evl1sca  22494  evl1var  22496  pf1mpf  22512  pf1ind  22515  mat0dimbas0  22623  mavmul0g  22710  hmph0  23952  tdeglem2  26218  deg1ldg  26249  deg1leb  26252  deg1val  26253  old1  28058  fply1  33848  selvply1rhmlema  33908  selvply1rhmlemb  33909  selvply1rhmlem1  33910  selvply1rhm0  33916  bnj105  35113  bnj96  35253  bnj98  35255  bnj149  35263  r11  35487  r12  35488  fineqvnttrclselem1  35534  rankeq1o  36663  nmulrid  36689  ordcmp  36978  ssoninhaus  36979  onint1  36980  poimirlem28  38319  reheibor  38510  wopprc  43777  pwslnmlem0  43838  pwfi2f1o  43843  nadd1suc  44139  lincval0  49215  lco0  49227  linds0  49265  f1omo  49691  setc1oterm  50289  setc1ohomfval  50291  setc1ocofval  50292  funcsetc1o  50295  isinito2lem  50296  setc1onsubc  50400