Definition df-1o 6577

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

This definition is referenced by:  1on  6584  df1o2  6591  ordgt0ge1  6598  oa1suc  6630  1onn  6683  nnm1  6688  nlt1pig  7554  indpi  7555  1tonninf  10696  hash1  11068  012of  16542  2o01f  16543  pwle2  16549  isomninnlem  16584  iswomninnlem  16603  ismkvnnlem  16606