Definition df-1o 7520

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 7513	. 2 class 1𝑜
2		c0 3897	. . 3 class ∅
3	2	csuc 5694	. 2 class suc ∅
4	1, 3	wceq 1480	1 wff 1𝑜 = suc ∅

This definition is referenced by:  1on  7527  df1o2  7532  ordgt0ge1  7537  oa1suc  7571  om1  7582  oe1  7584  oelim2  7635  nnecl  7653  1onn  7679  omabs  7687  nnm1  7688  0sdom1dom  8118  ackbij1lem14  9015  aleph1  9353  cfpwsdom  9366  nlt1pi  9688  indpi  9689  hash1  13148  aleph1re  14918  bnj168  30559  sltval2  31563  sltsolem1  31581  nosepnelem  31618  rankeq1o  31973  bj-1ex  32638  finxp1o  32900  finxpreclem4  32902  finxp00  32910  clsk1indlem1  37864