Theorem df1o2 8392

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 8385	. 2 ⊢ 1o = suc ∅
2		suc0 6383	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2754	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1541  ∅c0 4280  {csn 4573  suc csuc 6308  1_oc1o 8378

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-un 3902  df-nul 4281  df-suc 6312  df-1o 8385

This theorem is referenced by:  df2o3  8393  df2o2  8394  1oex  8395  1n0  8403  nlim1  8404  el1o  8410  dif1o  8415  0we1  8421  oeeui  8517  map0e  8806  ensn1  8943  en1  8946  map1  8962  xp1en  8976  0sdom1dom  9130  1sdom2  9132  sdom1  9134  1sdom2dom  9138  ssttrcl  9605  ttrclss  9610  ttrclselem2  9616  infxpenlem  9904  fseqenlem1  9915  dju1dif  10064  infdju1  10081  pwdju1  10082  infmap2  10108  cflim2  10154  pwxpndom2  10556  pwdjundom  10558  gchxpidm  10560  wuncval2  10638  tsk1  10655  hashen1  14277  sylow2alem2  19530  psr1baslem  22097  fvcoe1  22120  coe1f2  22122  coe1sfi  22126  coe1add  22178  coe1mul2lem1  22181  coe1mul2lem2  22182  coe1mul2  22183  coe1tm  22187  ply1coe  22213  evls1rhmlem  22236  evl1sca  22249  evl1var  22251  pf1mpf  22267  pf1ind  22270  mat0dimbas0  22381  mavmul0g  22468  hmph0  23710  tdeglem2  25993  deg1ldg  26024  deg1leb  26027  deg1val  26028  old1  27820  fply1  33521  bnj105  34736  bnj96  34877  bnj98  34879  bnj149  34887  r11  35105  r12  35106  fineqvnttrclselem1  35141  rankeq1o  36215  ordcmp  36491  ssoninhaus  36492  onint1  36493  poimirlem28  37698  reheibor  37889  wopprc  43133  pwslnmlem0  43194  pwfi2f1o  43199  nadd1suc  43495  lincval0  48526  lco0  48538  linds0  48576  f1omo  49003  setc1oterm  49602  setc1ohomfval  49604  setc1ocofval  49605  funcsetc1o  49608  isinito2lem  49609  setc1onsubc  49713