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 4263	. . 3 class ∅
3	2	csuc 6315	. 2 class suc ∅
4	1, 3	wceq 1548	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  9630  ssttrcl  9631  ttrcltr  9632  ttrclss  9636  dmttrcl  9637  rnttrcl  9638  ttrclselem2  9642  ackbij1lem14  10149  aleph1  10490  cfpwsdom  10503  nlt1pi  10825  indpi  10826  hash1  14361  aleph1re  16207  ltsval2  27640  ltssolem1  27659  nosepnelem  27663  nolt02o  27679  bday1  27826  cuteq1  27829  om2noseqlt  28311  bdaypw2n0bndlem  28475  bnj168  34926  r11  35288  satfv1  35604  fmla1  35628  rankeq1o  36412  finxp1o  37767  finxpreclem4  37769  finxp00  37777  ordeldif1o  43718  onov0suclim  43732  omabs2  43790  tfsconcatb0  43802  nlim1NEW  43899  aleph1min  44014  clsk1indlem1  44502