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  7713  indpi  7714  1tonninf  10897  hash1  11272  012of  17237  2o01f  17238  pwle2  17242  isomninnlem  17294  iswomninnlem  17315  ismkvnnlem  17318