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  27893  ltssolem1  27912  nosepnelem  27916  nolt02o  27932  bday1  28080  cuteq1  28083  om2noseqlt  28565  bdaypw2n0bndlem  28729  bnj168  35242  r11  35603  satfv1  35944  fmla1  35968  rankeq1o  36753  finxp1o  38148  finxpreclem4  38150  finxp00  38158  ordeldif1o  44103  onov0suclim  44117  omabs2  44175  tfsconcatb0  44187  nlim1NEW  44284  aleph1min  44399  clsk1indlem1  44887