Definition df-1o 6646

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 6639	. 2 class 1o
2		c0 3507	. . 3 class ∅
3	2	csuc 4485	. 2 class suc ∅
4	1, 3	wceq 1398	1 wff 1o = suc ∅

This definition is referenced by:  1on  6653  df1o2  6660  ordgt0ge1  6667  oa1suc  6699  1onn  6752  nnm1  6757  nlt1pig  7655  indpi  7656  1tonninf  10802  hash1  11174  012of  16759  2o01f  16760  pwle2  16764  isomninnlem  16806  iswomninnlem  16826  ismkvnnlem  16829