Definition df-1o 6573

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

This definition is referenced by:  1on  6580  df1o2  6587  ordgt0ge1  6594  oa1suc  6626  1onn  6679  nnm1  6684  nlt1pig  7544  indpi  7545  1tonninf  10680  hash1  11051  012of  16470  2o01f  16471  pwle2  16477  isomninnlem  16512  iswomninnlem  16531  ismkvnnlem  16534