Definition df-1o 6681

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 6674	. 2 class 1o
2		c0 3520	. . 3 class ∅
3	2	csuc 4508	. 2 class suc ∅
4	1, 3	wceq 1402	1 wff 1o = suc ∅

This definition is referenced by:  1on  6688  df1o2  6695  ordgt0ge1  6702  oa1suc  6734  1onn  6787  nnm1  6792  nlt1pig  7702  indpi  7703  1tonninf  10861  hash1  11235  012of  17006  2o01f  17007  pwle2  17011  isomninnlem  17053  iswomninnlem  17073  ismkvnnlem  17076