Definition df-1o 6471

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 6464	. 2 class 1o
2		c0 3447	. . 3 class (/)
3	2	csuc 4397	. 2 class suc (/)
4	1, 3	wceq 1364	1 wff 1o = suc (/)

This definition is referenced by:  1on  6478  df1o2  6484  ordgt0ge1  6490  oa1suc  6522  1onn  6575  nnm1  6580  nlt1pig  7403  indpi  7404  1tonninf  10515  hash1  10885  012of  15556  2o01f  15557  pwle2  15559  isomninnlem  15590  iswomninnlem  15609  ismkvnnlem  15612