Definition df-1o 6692

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 6685	. 2 class 1o
2		c0 3520	. . 3 class (/)
3	2	csuc 4512	. 2 class suc (/)
4	1, 3	wceq 1402	1 wff 1o = suc (/)

This definition is used by:  1on  6699  df1o2  6706  ordgt0ge1  6713  oa1suc  6745  1onn  6798  nnm1  6803  nlt1pig  7714  indpi  7715  1tonninf  10898  hash1  11273  012of  17245  2o01f  17246  pwle2  17250  isomninnlem  17302  iswomninnlem  17323  ismkvnnlem  17326