Definition df-1o 6483

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

This definition is referenced by:  1on  6490  df1o2  6496  ordgt0ge1  6502  oa1suc  6534  1onn  6587  nnm1  6592  nlt1pig  7427  indpi  7428  1tonninf  10552  hash1  10922  012of  15748  2o01f  15749  pwle2  15753  isomninnlem  15787  iswomninnlem  15806  ismkvnnlem  15809