Definition df-1o 6469

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 6462	. 2 class 1o
2		c0 3446	. . 3 class ∅
3	2	csuc 4396	. 2 class suc ∅
4	1, 3	wceq 1364	1 wff 1o = suc ∅

This definition is referenced by:  1on  6476  df1o2  6482  ordgt0ge1  6488  oa1suc  6520  1onn  6573  nnm1  6578  nlt1pig  7401  indpi  7402  1tonninf  10512  hash1  10882  012of  15486  2o01f  15487  pwle2  15489  isomninnlem  15520  iswomninnlem  15539  ismkvnnlem  15542