Definition df-1o 8466

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

This definition is referenced by:  df1o2  8473  1on  8478  1onOLD  8479  ordgt0ge1  8493  oa1suc  8531  o2p2e4  8541  om1  8542  oe1  8544  oelim2  8595  nnecl  8613  1onnALT  8640  omabs  8650  nnm1  8651  0sdom1domALT  9239  brttrcl2  9709  ssttrcl  9710  ttrcltr  9711  ttrclss  9715  dmttrcl  9716  rnttrcl  9717  ttrclselem2  9721  ackbij1lem14  10228  aleph1  10566  cfpwsdom  10579  nlt1pi  10901  indpi  10902  hash1  14364  aleph1re  16188  sltval2  27159  sltsolem1  27178  nosepnelem  27182  nolt02o  27198  bday1s  27332  cuteq1  27334  bnj168  33741  satfv1  34354  fmla1  34378  rankeq1o  35143  finxp1o  36273  finxpreclem4  36275  finxp00  36283  ordeldif1o  42010  onov0suclim  42024  omabs2  42082  tfsconcatb0  42094  nlim1NEW  42193  aleph1min  42308  clsk1indlem1  42796