Definition df-1o 8487

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 8480	. 2 class 1o
2		c0 4322	. . 3 class ∅
3	2	csuc 6373	. 2 class suc ∅
4	1, 3	wceq 1533	1 wff 1o = suc ∅

This definition is referenced by:  df1o2  8494  1on  8499  1onOLD  8500  ordgt0ge1  8514  oa1suc  8552  o2p2e4  8562  om1  8563  oe1  8565  oelim2  8616  nnecl  8634  1onnALT  8662  omabs  8672  nnm1  8673  0sdom1domALT  9267  brttrcl2  9744  ssttrcl  9745  ttrcltr  9746  ttrclss  9750  dmttrcl  9751  rnttrcl  9752  ttrclselem2  9756  ackbij1lem14  10263  aleph1  10601  cfpwsdom  10614  nlt1pi  10936  indpi  10937  hash1  14404  aleph1re  16230  sltval2  27640  sltsolem1  27659  nosepnelem  27663  nolt02o  27679  bday1s  27815  cuteq1  27817  om2noseqlt  28227  bnj168  34494  satfv1  35106  fmla1  35130  rankeq1o  35900  finxp1o  37004  finxpreclem4  37006  finxp00  37014  ordeldif1o  42833  onov0suclim  42847  omabs2  42905  tfsconcatb0  42917  nlim1NEW  43016  aleph1min  43131  clsk1indlem1  43619