Definition df-1o 8454

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

This definition is used by:  df1o2  8461  1on  8467  1n0  8473  ordgt0ge1  8479  oa1suc  8517  o2p2e4  8527  om1  8528  oe1  8530  oelim2  8582  nnecl  8600  1onnALT  8628  omabs  8638  nnm1  8639  0sdom1domALT  9216  brttrcl2  9693  ssttrcl  9694  ttrcltr  9695  ttrclss  9699  dmttrcl  9700  rnttrcl  9701  ttrclselem2  9705  ackbij1lem14  10281  aleph1  10627  cfpwsdom  10640  nlt1pi  10962  indpi  10963  hash1  14515  aleph1re  16380  ltsval2  27946  ltssolem1  27965  nosepnelem  27969  nolt02o  27985  bday1  28133  cuteq1  28136  om2noseqlt  28618  bdaypw2n0bndlem  28782  bnj168  35295  r11  35655  satfv1  36049  fmla1  36073  rankeq1o  36854  finxp1o  38235  finxpreclem4  38237  finxp00  38245  ordeldif1o  44205  onov0suclim  44219  omabs2  44277  tfsconcatb0  44289  nlim1NEW  44386  aleph1min  44501  clsk1indlem1  44989