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 4283	. . 3 class ∅
3	2	csuc 6317	. 2 class suc ∅
4	1, 3	wceq 1541	1 wff 1o = suc ∅

This definition is referenced by:  df1o2  8402  1on  8407  ordgt0ge1  8418  oa1suc  8456  o2p2e4  8466  om1  8467  oe1  8469  oelim2  8521  nnecl  8539  1onnALT  8567  omabs  8577  nnm1  8578  0sdom1domALT  9145  brttrcl2  9621  ssttrcl  9622  ttrcltr  9623  ttrclss  9627  dmttrcl  9628  rnttrcl  9629  ttrclselem2  9633  ackbij1lem14  10140  aleph1  10480  cfpwsdom  10493  nlt1pi  10815  indpi  10816  hash1  14325  aleph1re  16168  sltval2  27622  sltsolem1  27641  nosepnelem  27645  nolt02o  27661  bday1s  27802  cuteq1  27805  om2noseqlt  28260  bdaypw2n0s  28420  bnj168  34835  r11  35199  satfv1  35506  fmla1  35530  rankeq1o  36314  finxp1o  37536  finxpreclem4  37538  finxp00  37546  ordeldif1o  43444  onov0suclim  43458  omabs2  43516  tfsconcatb0  43528  nlim1NEW  43625  aleph1min  43740  clsk1indlem1  44228