Definition df-1o 8452

Description: Define the ordinal number 1. Definition 2.1 of [Schloeder] p. 4. (Contributed by NM, 29-Oct-1995.)

Assertion

Ref	Expression
df-1o	⊢ 1o = suc ∅

Detailed syntax breakdown of Definition df-1o

Step	Hyp	Ref	Expression
1		c1o 8445	. 2 class 1o
2		c0 4285	. . 3 class ∅
3	2	csuc 6362	. 2 class suc ∅
4	1, 3	wceq 1568	1 wff 1o = suc ∅

This definition is referenced by:  df1o2  8459  1on  8465  1n0  8471  ordgt0ge1  8477  oa1suc  8515  o2p2e4  8525  om1  8526  oe1  8528  oelim2  8580  nnecl  8598  1onnALT  8626  omabs  8636  nnm1  8637  0sdom1domALT  9206  brttrcl2  9682  ssttrcl  9683  ttrcltr  9684  ttrclss  9688  dmttrcl  9689  rnttrcl  9690  ttrclselem2  9694  ackbij1lem14  10214  aleph1  10555  cfpwsdom  10568  nlt1pi  10890  indpi  10891  hash1  14439  aleph1re  16300  ltsval2  27796  ltssolem1  27815  nosepnelem  27819  nolt02o  27835  bday1  27983  cuteq1  27986  om2noseqlt  28468  bdaypw2n0bndlem  28632  bnj168  35085  r11  35451  satfv1  35809  fmla1  35833  rankeq1o  36617  finxp1o  37982  finxpreclem4  37984  finxp00  37992  ordeldif1o  43935  onov0suclim  43949  omabs2  44007  tfsconcatb0  44019  nlim1NEW  44116  aleph1min  44231  clsk1indlem1  44719