Definition df-1o 8451

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 8444	. 2 class 1o
2		c0 4285	. . 3 class ∅
3	2	csuc 6362	. 2 class suc ∅
4	1, 3	wceq 1569	1 wff 1o = suc ∅

This definition is used by:  df1o2  8458  1on  8464  1n0  8470  ordgt0ge1  8476  oa1suc  8514  o2p2e4  8524  om1  8525  oe1  8527  oelim2  8579  nnecl  8597  1onnALT  8625  omabs  8635  nnm1  8636  0sdom1domALT  9205  brttrcl2  9681  ssttrcl  9682  ttrcltr  9683  ttrclss  9687  dmttrcl  9688  rnttrcl  9689  ttrclselem2  9693  ackbij1lem14  10222  aleph1  10562  cfpwsdom  10575  nlt1pi  10897  indpi  10898  hash1  14447  aleph1re  16307  ltsval2  27831  ltssolem1  27850  nosepnelem  27854  nolt02o  27870  bday1  28018  cuteq1  28021  om2noseqlt  28503  bdaypw2n0bndlem  28667  bnj168  35128  r11  35496  satfv1  35863  fmla1  35887  rankeq1o  36671  finxp1o  38066  finxpreclem4  38068  finxp00  38076  ordeldif1o  44015  onov0suclim  44029  omabs2  44087  tfsconcatb0  44099  nlim1NEW  44196  aleph1min  44311  clsk1indlem1  44799