Definition df-1o 8409

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

This definition is referenced by:  df1o2  8416  1on  8421  ordgt0ge1  8432  oa1suc  8470  o2p2e4  8480  om1  8481  oe1  8483  oelim2  8535  nnecl  8553  1onnALT  8581  omabs  8591  nnm1  8592  0sdom1domALT  9161  brttrcl2  9637  ssttrcl  9638  ttrcltr  9639  ttrclss  9643  dmttrcl  9644  rnttrcl  9645  ttrclselem2  9649  ackbij1lem14  10156  aleph1  10496  cfpwsdom  10509  nlt1pi  10831  indpi  10832  hash1  14341  aleph1re  16184  ltsval2  27641  ltssolem1  27660  nosepnelem  27664  nolt02o  27680  bday1  27827  cuteq1  27830  om2noseqlt  28312  bdaypw2n0bndlem  28476  bnj168  34913  r11  35277  satfv1  35585  fmla1  35609  rankeq1o  36393  finxp1o  37674  finxpreclem4  37676  finxp00  37684  ordeldif1o  43646  onov0suclim  43660  omabs2  43718  tfsconcatb0  43730  nlim1NEW  43827  aleph1min  43942  clsk1indlem1  44430