Definition df-1o 6384

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 6377	. 2 class 1o
2		c0 3409	. . 3 class ∅
3	2	csuc 4343	. 2 class suc ∅
4	1, 3	wceq 1343	1 wff 1o = suc ∅

This definition is referenced by:  1on  6391  df1o2  6397  ordgt0ge1  6403  oa1suc  6435  1onn  6488  nnm1  6492  nlt1pig  7282  indpi  7283  1tonninf  10375  hash1  10724  012of  13875  2o01f  13876  pwle2  13878  isomninnlem  13909  iswomninnlem  13928  ismkvnnlem  13931