Definition df-1o 8478

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

This definition is referenced by:  df1o2  8485  1on  8490  1onOLD  8491  ordgt0ge1  8503  oa1suc  8541  o2p2e4  8551  om1  8552  oe1  8554  oelim2  8605  nnecl  8623  1onnALT  8651  omabs  8661  nnm1  8662  0sdom1domALT  9245  brttrcl2  9726  ssttrcl  9727  ttrcltr  9728  ttrclss  9732  dmttrcl  9733  rnttrcl  9734  ttrclselem2  9738  ackbij1lem14  10244  aleph1  10583  cfpwsdom  10596  nlt1pi  10918  indpi  10919  hash1  14420  aleph1re  16261  sltval2  27618  sltsolem1  27637  nosepnelem  27641  nolt02o  27657  bday1s  27793  cuteq1  27795  om2noseqlt  28222  bnj168  34707  satfv1  35331  fmla1  35355  rankeq1o  36135  finxp1o  37356  finxpreclem4  37358  finxp00  37366  ordeldif1o  43231  onov0suclim  43245  omabs2  43303  tfsconcatb0  43315  nlim1NEW  43413  aleph1min  43528  clsk1indlem1  44016