Theorem df1o2 8460

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 8453	. 2 ⊢ 1o = suc ∅
2		suc0 6439	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2792	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1567  ∅c0 4294  {csn 4594  suc csuc 6363  1_oc1o 8446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-un 3918  df-nul 4295  df-suc 6367  df-1o 8453

This theorem is referenced by:  df2o3  8461  df2o2  8462  1oex  8463  1n0OLD  8473  nlim1  8474  el1o  8480  dif1o  8485  0we1  8491  oeeui  8588  map0e  8880  ensn1  9018  en1  9021  map1  9037  xp1en  9051  0sdom1dom  9206  1sdom2  9208  sdom1  9210  1sdom2dom  9214  ssttrcl  9684  ttrclss  9689  ttrclselem2  9695  infxpenlem  9997  fseqenlem1  10008  dju1dif  10156  infdju1  10173  pwdju1  10174  infmap2  10200  cflim2  10247  pwxpndom2  10650  pwdjundom  10652  gchxpidm  10654  wuncval2  10732  tsk1  10749  hashen1  14406  sylow2alem2  19688  psr1baslem  22314  fvcoe1  22336  coe1f2  22338  coe1sfi  22342  coe1add  22394  coe1mul2lem1  22397  coe1mul2lem2  22398  coe1mul2  22399  coe1tm  22403  ply1coe  22427  evls1rhmlem  22450  evl1sca  22463  evl1var  22465  pf1mpf  22481  pf1ind  22484  mat0dimbas0  22592  mavmul0g  22679  hmph0  23921  tdeglem2  26187  deg1ldg  26218  deg1leb  26221  deg1val  26222  old1  28024  fply1  33793  selvply1rhmlema  33853  selvply1rhmlemb  33854  selvply1rhmlem1  33855  selvply1rhm0  33861  bnj105  35058  bnj96  35198  bnj98  35200  bnj149  35208  r11  35430  r12  35431  fineqvnttrclselem1  35467  rankeq1o  36596  ordcmp  36881  ssoninhaus  36882  onint1  36883  poimirlem28  38221  reheibor  38412  wopprc  43683  pwslnmlem0  43744  pwfi2f1o  43749  nadd1suc  44045  lincval0  49114  lco0  49126  linds0  49164  f1omo  49590  setc1oterm  50188  setc1ohomfval  50190  setc1ocofval  50191  funcsetc1o  50194  isinito2lem  50195  setc1onsubc  50299