Definition df-1o 6321

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 6314	. 2 class 1o
2		c0 3368	. . 3 class ∅
3	2	csuc 4295	. 2 class suc ∅
4	1, 3	wceq 1332	1 wff 1o = suc ∅

This definition is referenced by:  1on  6328  df1o2  6334  ordgt0ge1  6340  oa1suc  6371  1onn  6424  nnm1  6428  nlt1pig  7173  indpi  7174  1tonninf  10244  hash1  10589  012of  13363  2o01f  13364  pwle2  13366  isomninnlem  13400  iswomninnlem  13417  ismkvnnlem  13419