Definition df-1o 7897

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 7890	. 2 class 1o
2		c0 4173	. . 3 class ∅
3	2	csuc 6025	. 2 class suc ∅
4	1, 3	wceq 1507	1 wff 1o = suc ∅

This definition is referenced by:  1on  7904  df1o2  7910  ordgt0ge1  7916  oa1suc  7950  om1  7961  oe1  7963  oelim2  8014  nnecl  8032  1onn  8058  omabs  8066  nnm1  8067  0sdom1dom  8503  ackbij1lem14  9445  aleph1  9783  cfpwsdom  9796  nlt1pi  10118  indpi  10119  hash1  13569  aleph1re  15448  bnj168  31609  sltval2  32624  sltsolem1  32641  nosepnelem  32645  nolt02o  32660  rankeq1o  33093  finxp1o  34049  finxpreclem4  34051  finxp00  34059  clsk1indlem1  39703