Theorem df1o2 8473

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 8466	. 2 ⊢ 1o = suc ∅
2		suc0 6440	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2761	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1542  ∅c0 4323  {csn 4629  suc csuc 6367  1_oc1o 8459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-un 3954  df-nul 4324  df-suc 6371  df-1o 8466

This theorem is referenced by:  df2o3  8474  df2o2  8475  1oex  8476  1n0  8488  nlim1  8489  el1o  8495  dif1o  8500  0we1  8506  oeeui  8602  map0e  8876  ensn1  9017  ensn1OLD  9018  en1  9021  en1OLD  9022  map1  9040  xp1en  9057  0sdom1dom  9238  1sdom2  9240  sdom1  9242  1sdom2dom  9247  pwfiOLD  9347  ssttrcl  9710  ttrclss  9715  ttrclselem2  9721  infxpenlem  10008  fseqenlem1  10019  dju1dif  10167  infdju1  10184  pwdju1  10185  infmap2  10213  cflim2  10258  pwxpndom2  10660  pwdjundom  10662  gchxpidm  10664  wuncval2  10742  tsk1  10759  hashen1  14330  sylow2alem2  19486  psr1baslem  21709  fvcoe1  21731  coe1f2  21733  coe1sfi  21737  coe1add  21786  coe1mul2lem1  21789  coe1mul2lem2  21790  coe1mul2  21791  coe1tm  21795  ply1coe  21820  evls1rhmlem  21840  evl1sca  21853  evl1var  21855  pf1mpf  21871  pf1ind  21874  mat0dimbas0  21968  mavmul0g  22055  hmph0  23299  tdeglem2  25579  deg1ldg  25610  deg1leb  25613  deg1val  25614  old1  27370  fply1  32637  bnj105  33735  bnj96  33876  bnj98  33878  bnj149  33886  rankeq1o  35143  ordcmp  35332  ssoninhaus  35333  onint1  35334  poimirlem28  36516  reheibor  36707  wopprc  41769  pwslnmlem0  41833  pwfi2f1o  41838  nadd1suc  42142  lincval0  47096  lco0  47108  linds0  47146