Definition df-1o 8328

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 8321	. 2 class 1o
2		c0 4262	. . 3 class ∅
3	2	csuc 6283	. 2 class suc ∅
4	1, 3	wceq 1539	1 wff 1o = suc ∅

This definition is referenced by:  df1o2  8335  1on  8340  1onOLD  8341  ordgt0ge1  8354  oa1suc  8392  o2p2e4  8402  om1  8404  oe1  8406  oelim2  8457  nnecl  8475  1onnALT  8502  omabs  8512  nnm1  8513  0sdom1domOLD  9060  brttrcl2  9516  ssttrcl  9517  ttrcltr  9518  ttrclss  9522  dmttrcl  9523  rnttrcl  9524  ttrclselem2  9528  ackbij1lem14  10035  aleph1  10373  cfpwsdom  10386  nlt1pi  10708  indpi  10709  hash1  14164  aleph1re  15999  bnj168  32754  satfv1  33370  fmla1  33394  sltval2  33904  sltsolem1  33923  nosepnelem  33927  nolt02o  33943  bday1s  34070  rankeq1o  34518  finxp1o  35607  finxpreclem4  35609  finxp00  35617  nlim1NEW  41087  aleph1min  41202  clsk1indlem1  41693