Definition df-1o 6677

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 6670	. 2 class 1o
2		c0 3520	. . 3 class ∅
3	2	csuc 4505	. 2 class suc ∅
4	1, 3	wceq 1402	1 wff 1o = suc ∅

This definition is referenced by:  1on  6684  df1o2  6691  ordgt0ge1  6698  oa1suc  6730  1onn  6783  nnm1  6788  nlt1pig  7698  indpi  7699  1tonninf  10856  hash1  11230  012of  16937  2o01f  16938  pwle2  16942  isomninnlem  16984  iswomninnlem  17004  ismkvnnlem  17007