Definition df-1o 6582

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 6575	. 2 class 1o
2		c0 3494	. . 3 class ∅
3	2	csuc 4462	. 2 class suc ∅
4	1, 3	wceq 1397	1 wff 1o = suc ∅

This definition is referenced by:  1on  6589  df1o2  6596  ordgt0ge1  6603  oa1suc  6635  1onn  6688  nnm1  6693  nlt1pig  7561  indpi  7562  1tonninf  10704  hash1  11076  012of  16618  2o01f  16619  pwle2  16625  isomninnlem  16660  iswomninnlem  16679  ismkvnnlem  16682