Definition df-1o 6568

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

This definition is referenced by:  1on  6575  df1o2  6582  ordgt0ge1  6589  oa1suc  6621  1onn  6674  nnm1  6679  nlt1pig  7536  indpi  7537  1tonninf  10671  hash1  11041  012of  16386  2o01f  16387  pwle2  16393  isomninnlem  16428  iswomninnlem  16447  ismkvnnlem  16450