Definition df-1o 6552

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 6545	. 2 class 1o
2		c0 3491	. . 3 class ∅
3	2	csuc 4453	. 2 class suc ∅
4	1, 3	wceq 1395	1 wff 1o = suc ∅

This definition is referenced by:  1on  6559  df1o2  6565  ordgt0ge1  6571  oa1suc  6603  1onn  6656  nnm1  6661  nlt1pig  7516  indpi  7517  1tonninf  10650  hash1  11020  012of  16288  2o01f  16289  pwle2  16295  isomninnlem  16329  iswomninnlem  16348  ismkvnnlem  16351