Definition df-1o 7727

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 7720	. 2 class 1𝑜
2		c0 4056	. . 3 class ∅
3	2	csuc 5884	. 2 class suc ∅
4	1, 3	wceq 1630	1 wff 1𝑜 = suc ∅

This definition is referenced by:  1on  7734  df1o2  7739  ordgt0ge1  7744  oa1suc  7778  om1  7789  oe1  7791  oelim2  7842  nnecl  7860  1onn  7886  omabs  7894  nnm1  7895  0sdom1dom  8321  ackbij1lem14  9245  aleph1  9583  cfpwsdom  9596  nlt1pi  9918  indpi  9919  hash1  13382  aleph1re  15171  bnj168  31103  sltval2  32113  sltsolem1  32130  nosepnelem  32134  nolt02o  32149  rankeq1o  32582  bj-1ex  33242  finxp1o  33538  finxpreclem4  33540  finxp00  33548  clsk1indlem1  38843