Definition df-1o 8434

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 8427	. 2 class 1o
2		c0 4296	. . 3 class ∅
3	2	csuc 6334	. 2 class suc ∅
4	1, 3	wceq 1540	1 wff 1o = suc ∅

This definition is referenced by:  df1o2  8441  1on  8446  ordgt0ge1  8457  oa1suc  8495  o2p2e4  8505  om1  8506  oe1  8508  oelim2  8559  nnecl  8577  1onnALT  8605  omabs  8615  nnm1  8616  0sdom1domALT  9186  brttrcl2  9667  ssttrcl  9668  ttrcltr  9669  ttrclss  9673  dmttrcl  9674  rnttrcl  9675  ttrclselem2  9679  ackbij1lem14  10185  aleph1  10524  cfpwsdom  10537  nlt1pi  10859  indpi  10860  hash1  14369  aleph1re  16213  sltval2  27568  sltsolem1  27587  nosepnelem  27591  nolt02o  27607  bday1s  27743  cuteq1  27746  om2noseqlt  28193  bnj168  34720  satfv1  35350  fmla1  35374  rankeq1o  36159  finxp1o  37380  finxpreclem4  37382  finxp00  37390  ordeldif1o  43249  onov0suclim  43263  omabs2  43321  tfsconcatb0  43333  nlim1NEW  43431  aleph1min  43546  clsk1indlem1  44034