Definition df-1o 8385

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 8378	. 2 class 1o
2		c0 4280	. . 3 class ∅
3	2	csuc 6308	. 2 class suc ∅
4	1, 3	wceq 1541	1 wff 1o = suc ∅

This definition is referenced by:  df1o2  8392  1on  8397  ordgt0ge1  8408  oa1suc  8446  o2p2e4  8456  om1  8457  oe1  8459  oelim2  8510  nnecl  8528  1onnALT  8556  omabs  8566  nnm1  8567  0sdom1domALT  9131  brttrcl2  9604  ssttrcl  9605  ttrcltr  9606  ttrclss  9610  dmttrcl  9611  rnttrcl  9612  ttrclselem2  9616  ackbij1lem14  10123  aleph1  10462  cfpwsdom  10475  nlt1pi  10797  indpi  10798  hash1  14311  aleph1re  16154  sltval2  27595  sltsolem1  27614  nosepnelem  27618  nolt02o  27634  bday1s  27775  cuteq1  27778  om2noseqlt  28229  bnj168  34742  r11  35105  satfv1  35407  fmla1  35431  rankeq1o  36213  finxp1o  37434  finxpreclem4  37436  finxp00  37444  ordeldif1o  43301  onov0suclim  43315  omabs2  43373  tfsconcatb0  43385  nlim1NEW  43483  aleph1min  43598  clsk1indlem1  44086