Definition df-1o 8399

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

This definition is referenced by:  df1o2  8406  1on  8411  ordgt0ge1  8422  oa1suc  8460  o2p2e4  8470  om1  8471  oe1  8473  oelim2  8525  nnecl  8543  1onnALT  8571  omabs  8581  nnm1  8582  0sdom1domALT  9151  brttrcl2  9627  ssttrcl  9628  ttrcltr  9629  ttrclss  9633  dmttrcl  9634  rnttrcl  9635  ttrclselem2  9639  ackbij1lem14  10146  aleph1  10486  cfpwsdom  10499  nlt1pi  10821  indpi  10822  hash1  14331  aleph1re  16174  ltsval2  27628  ltssolem1  27647  nosepnelem  27651  nolt02o  27667  bday1  27814  cuteq1  27817  om2noseqlt  28299  bdaypw2n0bndlem  28463  bnj168  34888  r11  35252  satfv1  35559  fmla1  35583  rankeq1o  36367  finxp1o  37599  finxpreclem4  37601  finxp00  37609  ordeldif1o  43569  onov0suclim  43583  omabs2  43641  tfsconcatb0  43653  nlim1NEW  43750  aleph1min  43865  clsk1indlem1  44353