Theorem df1o2 8494

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 8487	. 2 ⊢ 1o = suc ∅
2		suc0 6438	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2757	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1539  ∅c0 4313  {csn 4606  suc csuc 6365  1_oc1o 8480

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 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-dif 3934  df-un 3936  df-nul 4314  df-suc 6369  df-1o 8487

This theorem is referenced by:  df2o3  8495  df2o2  8496  1oex  8497  1n0  8507  nlim1  8508  el1o  8514  dif1o  8519  0we1  8525  oeeui  8621  map0e  8903  ensn1  9042  en1  9045  map1  9061  xp1en  9078  0sdom1dom  9255  1sdom2  9257  sdom1  9259  1sdom2dom  9264  ssttrcl  9736  ttrclss  9741  ttrclselem2  9747  infxpenlem  10034  fseqenlem1  10045  dju1dif  10194  infdju1  10211  pwdju1  10212  infmap2  10238  cflim2  10284  pwxpndom2  10686  pwdjundom  10688  gchxpidm  10690  wuncval2  10768  tsk1  10785  hashen1  14390  sylow2alem2  19603  psr1baslem  22133  fvcoe1  22156  coe1f2  22158  coe1sfi  22162  coe1add  22214  coe1mul2lem1  22217  coe1mul2lem2  22218  coe1mul2  22219  coe1tm  22223  ply1coe  22249  evls1rhmlem  22272  evl1sca  22285  evl1var  22287  pf1mpf  22303  pf1ind  22306  mat0dimbas0  22419  mavmul0g  22506  hmph0  23748  tdeglem2  26035  deg1ldg  26066  deg1leb  26069  deg1val  26070  old1  27849  fply1  33510  bnj105  34672  bnj96  34813  bnj98  34815  bnj149  34823  rankeq1o  36106  ordcmp  36382  ssoninhaus  36383  onint1  36384  poimirlem28  37589  reheibor  37780  wopprc  42980  pwslnmlem0  43041  pwfi2f1o  43046  nadd1suc  43343  lincval0  48266  lco0  48278  linds0  48316  setc1oterm  49091