Definition df-1o 8506

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

This definition is referenced by:  df1o2  8513  1on  8518  1onOLD  8519  ordgt0ge1  8531  oa1suc  8569  o2p2e4  8579  om1  8580  oe1  8582  oelim2  8633  nnecl  8651  1onnALT  8679  omabs  8689  nnm1  8690  0sdom1domALT  9275  brttrcl2  9754  ssttrcl  9755  ttrcltr  9756  ttrclss  9760  dmttrcl  9761  rnttrcl  9762  ttrclselem2  9766  ackbij1lem14  10272  aleph1  10611  cfpwsdom  10624  nlt1pi  10946  indpi  10947  hash1  14443  aleph1re  16281  sltval2  27701  sltsolem1  27720  nosepnelem  27724  nolt02o  27740  bday1s  27876  cuteq1  27878  om2noseqlt  28305  bnj168  34744  satfv1  35368  fmla1  35392  rankeq1o  36172  finxp1o  37393  finxpreclem4  37395  finxp00  37403  ordeldif1o  43273  onov0suclim  43287  omabs2  43345  tfsconcatb0  43357  nlim1NEW  43455  aleph1min  43570  clsk1indlem1  44058