Definition df-1o 8394

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

This definition is referenced by:  df1o2  8401  1on  8406  ordgt0ge1  8417  oa1suc  8455  o2p2e4  8465  om1  8466  oe1  8468  oelim2  8520  nnecl  8538  1onnALT  8566  omabs  8576  nnm1  8577  0sdom1domALT  9146  brttrcl2  9624  ssttrcl  9625  ttrcltr  9626  ttrclss  9630  dmttrcl  9631  rnttrcl  9632  ttrclselem2  9636  ackbij1lem14  10143  aleph1  10483  cfpwsdom  10496  nlt1pi  10818  indpi  10819  hash1  14355  aleph1re  16201  ltsval2  27608  ltssolem1  27627  nosepnelem  27631  nolt02o  27647  bday1  27794  cuteq1  27797  om2noseqlt  28279  bdaypw2n0bndlem  28443  bnj168  34861  r11  35225  satfv1  35533  fmla1  35557  rankeq1o  36341  finxp1o  37696  finxpreclem4  37698  finxp00  37706  ordeldif1o  43676  onov0suclim  43690  omabs2  43748  tfsconcatb0  43760  nlim1NEW  43857  aleph1min  43972  clsk1indlem1  44460