Definition df-1o 7560

Description: Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.)

Assertion

Ref	Expression
df-1o	⊢ 1𝑜 = suc ∅

Detailed syntax breakdown of Definition df-1o

Step	Hyp	Ref	Expression
1		c1o 7553	. 2 class 1𝑜
2		c0 3915	. . 3 class ∅
3	2	csuc 5725	. 2 class suc ∅
4	1, 3	wceq 1483	1 wff 1𝑜 = suc ∅

This definition is referenced by:  1on  7567  df1o2  7572  ordgt0ge1  7577  oa1suc  7611  om1  7622  oe1  7624  oelim2  7675  nnecl  7693  1onn  7719  omabs  7727  nnm1  7728  0sdom1dom  8158  ackbij1lem14  9055  aleph1  9393  cfpwsdom  9406  nlt1pi  9728  indpi  9729  hash1  13192  aleph1re  14974  bnj168  30798  sltval2  31809  sltsolem1  31826  nosepnelem  31830  nolt02o  31845  rankeq1o  32278  bj-1ex  32938  finxp1o  33229  finxpreclem4  33231  finxp00  33239  clsk1indlem1  38343