Definition df-1o 8402

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 8395	. 2 class 1o
2		c0 4274	. . 3 class ∅
3	2	csuc 6323	. 2 class suc ∅
4	1, 3	wceq 1542	1 wff 1o = suc ∅

This definition is referenced by:  df1o2  8409  1on  8414  ordgt0ge1  8425  oa1suc  8463  o2p2e4  8473  om1  8474  oe1  8476  oelim2  8528  nnecl  8546  1onnALT  8574  omabs  8584  nnm1  8585  0sdom1domALT  9154  brttrcl2  9632  ssttrcl  9633  ttrcltr  9634  ttrclss  9638  dmttrcl  9639  rnttrcl  9640  ttrclselem2  9644  ackbij1lem14  10151  aleph1  10491  cfpwsdom  10504  nlt1pi  10826  indpi  10827  hash1  14363  aleph1re  16209  ltsval2  27617  ltssolem1  27636  nosepnelem  27640  nolt02o  27656  bday1  27803  cuteq1  27806  om2noseqlt  28288  bdaypw2n0bndlem  28452  bnj168  34870  r11  35234  satfv1  35542  fmla1  35566  rankeq1o  36350  finxp1o  37705  finxpreclem4  37707  finxp00  37715  ordeldif1o  43685  onov0suclim  43699  omabs2  43757  tfsconcatb0  43769  nlim1NEW  43866  aleph1min  43981  clsk1indlem1  44469