Definition df-1o 8458

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 8451	. 2 class 1o
2		c0 4282	. . 3 class ∅
3	2	csuc 6363	. 2 class suc ∅
4	1, 3	wceq 1570	1 wff 1o = suc ∅

This definition is used by:  df1o2  8465  1on  8471  1n0  8477  ordgt0ge1  8483  oa1suc  8521  o2p2e4  8531  om1  8532  oe1  8534  oelim2  8586  nnecl  8604  1onnALT  8632  omabs  8642  nnm1  8643  0sdom1domALT  9220  brttrcl2  9696  ssttrcl  9697  ttrcltr  9698  ttrclss  9702  dmttrcl  9703  rnttrcl  9704  ttrclselem2  9708  ackbij1lem14  10237  aleph1  10583  cfpwsdom  10596  nlt1pi  10918  indpi  10919  hash1  14470  aleph1re  16337  ltsval2  27890  ltssolem1  27909  nosepnelem  27913  nolt02o  27929  bday1  28077  cuteq1  28080  om2noseqlt  28562  bdaypw2n0bndlem  28726  bnj168  35227  r11  35588  satfv1  35929  fmla1  35953  rankeq1o  36738  finxp1o  38133  finxpreclem4  38135  finxp00  38143  ordeldif1o  44088  onov0suclim  44102  omabs2  44160  tfsconcatb0  44172  nlim1NEW  44269  aleph1min  44384  clsk1indlem1  44872