Definition df-1o 8281

Description: Define the ordinal number 1. (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 8274	. 2 class 1o
2		c0 4261	. . 3 class ∅
3	2	csuc 6265	. 2 class suc ∅
4	1, 3	wceq 1541	1 wff 1o = suc ∅

This definition is referenced by:  1on  8288  df1o2  8293  ordgt0ge1  8303  oa1suc  8337  o2p2e4  8347  om1  8349  oe1  8351  oelim2  8402  nnecl  8420  1onn  8446  omabs  8455  nnm1  8456  0sdom1dom  8982  brttrcl2  9433  ssttrcl  9434  ttrcltr  9435  ttrclss  9439  dmttrcl  9440  rnttrcl  9441  ttrclselem2  9445  ackbij1lem14  9973  aleph1  10311  cfpwsdom  10324  nlt1pi  10646  indpi  10647  hash1  14100  aleph1re  15935  bnj168  32688  satfv1  33304  fmla1  33328  sltval2  33838  sltsolem1  33857  nosepnelem  33861  nolt02o  33877  bday1s  34004  rankeq1o  34452  finxp1o  35542  finxpreclem4  35544  finxp00  35552  aleph1min  41117  clsk1indlem1  41608