Theorem df1o2 8521

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 8514	. 2 ⊢ 1o = suc ∅
2		suc0 6467	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2765	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1539  ∅c0 4342  {csn 4634  suc csuc 6394  1_oc1o 8507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3483  df-dif 3969  df-un 3971  df-nul 4343  df-suc 6398  df-1o 8514

This theorem is referenced by:  df2o3  8522  df2o2  8523  1oex  8524  1n0  8534  nlim1  8535  el1o  8541  dif1o  8546  0we1  8552  oeeui  8648  map0e  8930  ensn1  9069  en1  9072  map1  9088  xp1en  9105  0sdom1dom  9281  1sdom2  9283  sdom1  9285  1sdom2dom  9290  ssttrcl  9762  ttrclss  9767  ttrclselem2  9773  infxpenlem  10060  fseqenlem1  10071  dju1dif  10220  infdju1  10237  pwdju1  10238  infmap2  10264  cflim2  10310  pwxpndom2  10712  pwdjundom  10714  gchxpidm  10716  wuncval2  10794  tsk1  10811  hashen1  14415  sylow2alem2  19660  psr1baslem  22211  fvcoe1  22234  coe1f2  22236  coe1sfi  22240  coe1add  22292  coe1mul2lem1  22295  coe1mul2lem2  22296  coe1mul2  22297  coe1tm  22301  ply1coe  22327  evls1rhmlem  22350  evl1sca  22363  evl1var  22365  pf1mpf  22381  pf1ind  22384  mat0dimbas0  22497  mavmul0g  22584  hmph0  23828  tdeglem2  26126  deg1ldg  26157  deg1leb  26160  deg1val  26161  old1  27940  fply1  33596  bnj105  34731  bnj96  34872  bnj98  34874  bnj149  34882  rankeq1o  36166  ordcmp  36442  ssoninhaus  36443  onint1  36444  poimirlem28  37649  reheibor  37840  wopprc  43035  pwslnmlem0  43096  pwfi2f1o  43101  nadd1suc  43398  lincval0  48299  lco0  48311  linds0  48349