Definition df-1o 6625

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

This definition is referenced by:  1on  6632  df1o2  6639  ordgt0ge1  6646  oa1suc  6678  1onn  6731  nnm1  6736  nlt1pig  7604  indpi  7605  1tonninf  10747  hash1  11119  012of  16693  2o01f  16694  pwle2  16700  isomninnlem  16742  iswomninnlem  16762  ismkvnnlem  16765