Theorem df1o2 8483

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

This proof depends on syntax axioms:   = wceq 1570  ∅c0 4279  {csn 4584  suc csuc 6364  1_oc1o 8469

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-un 3904  df-nul 4280  df-suc 6368  df-1o 8476

This theorem is used by:  df2o3  8484  df2o2  8485  1oex  8486  1n0OLD  8496  nlim1  8497  el1o  8503  dif1o  8508  0we1  8514  oeeui  8611  map0e  8910  ensn1  9048  en1  9051  map1  9068  xp1en  9082  0sdom1dom  9237  1sdom2  9239  sdom1  9241  1sdom2dom  9245  ssttrcl  9716  ttrclss  9721  ttrclselem2  9727  infxpenlem  10092  fseqenlem1  10103  dju1dif  10251  infdju1  10268  pwdju1  10269  infmap2  10295  cflim2  10341  pwxpndom2  10750  pwdjundom  10752  gchxpidm  10754  wuncval2  10832  tsk1  10849  hashen1  14514  sylow2alem2  19832  psr1baslem  22503  fvcoe1  22525  coe1f2  22527  coe1sfi  22531  coe1add  22583  coe1mul2lem1  22586  coe1mul2lem2  22587  coe1mul2  22588  coe1tm  22592  ply1coe  22616  evls1rhmlem  22639  evl1sca  22652  evl1var  22654  pf1mpf  22670  pf1ind  22673  mat0dimbas0  22781  mavmul0g  22868  hmph0  24114  tdeglem2  26379  deg1ldg  26410  deg1leb  26413  deg1val  26414  old1  28251  fply1  34090  selvply1rhmlema  34150  selvply1rhmlemb  34151  selvply1rhmlem1  34152  selvply1rhm0  34158  bnj105  35355  bnj96  35495  bnj98  35497  bnj149  35505  r11  35725  r12  35726  fineqvnttrclselem1  35789  rankeq1o  36932  nmulrid  36946  ordcmp  37235  ssoninhaus  37236  onint1  37237  poimirlem28  38566  reheibor  38773  wopprc  44036  pwslnmlem0  44092  pwfi2f1o  44097  nadd1suc  44393  lincval0  49526  lco0  49538  linds0  49576  f1omo  50000  setc1oterm  50598  setc1ohomfval  50600  setc1ocofval  50601  funcsetc1o  50604  isinito2lem  50605  setc1onsubc  50709