Definition df-1o 8395

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 8388	. 2 class 1o
2		c0 4286	. . 3 class ∅
3	2	csuc 6313	. 2 class suc ∅
4	1, 3	wceq 1540	1 wff 1o = suc ∅

This definition is referenced by:  df1o2  8402  1on  8407  ordgt0ge1  8418  oa1suc  8456  o2p2e4  8466  om1  8467  oe1  8469  oelim2  8520  nnecl  8538  1onnALT  8566  omabs  8576  nnm1  8577  0sdom1domALT  9146  brttrcl2  9629  ssttrcl  9630  ttrcltr  9631  ttrclss  9635  dmttrcl  9636  rnttrcl  9637  ttrclselem2  9641  ackbij1lem14  10145  aleph1  10484  cfpwsdom  10497  nlt1pi  10819  indpi  10820  hash1  14329  aleph1re  16172  sltval2  27584  sltsolem1  27603  nosepnelem  27607  nolt02o  27623  bday1s  27763  cuteq1  27766  om2noseqlt  28216  bnj168  34699  satfv1  35338  fmla1  35362  rankeq1o  36147  finxp1o  37368  finxpreclem4  37370  finxp00  37378  ordeldif1o  43236  onov0suclim  43250  omabs2  43308  tfsconcatb0  43320  nlim1NEW  43418  aleph1min  43533  clsk1indlem1  44021