Theorem df1o2 8469

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 8462	. 2 ⊢ 1o = suc ∅
2		suc0 6436	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2760	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1541  ∅c0 4321  {csn 4627  suc csuc 6363  1_oc1o 8455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3950  df-un 3952  df-nul 4322  df-suc 6367  df-1o 8462

This theorem is referenced by:  df2o3  8470  df2o2  8471  1oex  8472  1n0  8484  nlim1  8485  el1o  8491  dif1o  8496  0we1  8502  oeeui  8598  map0e  8872  ensn1  9013  ensn1OLD  9014  en1  9017  en1OLD  9018  map1  9036  xp1en  9053  0sdom1dom  9234  1sdom2  9236  sdom1  9238  1sdom2dom  9243  pwfiOLD  9343  ssttrcl  9706  ttrclss  9711  ttrclselem2  9717  infxpenlem  10004  fseqenlem1  10015  dju1dif  10163  infdju1  10180  pwdju1  10181  infmap2  10209  cflim2  10254  pwxpndom2  10656  pwdjundom  10658  gchxpidm  10660  wuncval2  10738  tsk1  10755  hashen1  14326  sylow2alem2  19480  psr1baslem  21700  fvcoe1  21722  coe1f2  21724  coe1sfi  21728  coe1add  21777  coe1mul2lem1  21780  coe1mul2lem2  21781  coe1mul2  21782  coe1tm  21786  ply1coe  21811  evls1rhmlem  21831  evl1sca  21844  evl1var  21846  pf1mpf  21862  pf1ind  21865  mat0dimbas0  21959  mavmul0g  22046  hmph0  23290  tdeglem2  25570  deg1ldg  25601  deg1leb  25604  deg1val  25605  old1  27359  fply1  32625  bnj105  33723  bnj96  33864  bnj98  33866  bnj149  33874  rankeq1o  35131  ordcmp  35320  ssoninhaus  35321  onint1  35322  poimirlem28  36504  reheibor  36695  wopprc  41754  pwslnmlem0  41818  pwfi2f1o  41823  nadd1suc  42127  lincval0  47049  lco0  47061  linds0  47099