Definition df-1o 8102

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 8095	. 2 class 1o
2		c0 4291	. . 3 class ∅
3	2	csuc 6193	. 2 class suc ∅
4	1, 3	wceq 1537	1 wff 1o = suc ∅

This definition is referenced by:  1on  8109  df1o2  8116  ordgt0ge1  8122  oa1suc  8156  o2p2e4  8166  om1  8168  oe1  8170  oelim2  8221  nnecl  8239  1onn  8265  omabs  8274  nnm1  8275  0sdom1dom  8716  ackbij1lem14  9655  aleph1  9993  cfpwsdom  10006  nlt1pi  10328  indpi  10329  hash1  13766  aleph1re  15598  bnj168  32000  satfv1  32610  fmla1  32634  sltval2  33163  sltsolem1  33180  nosepnelem  33184  nolt02o  33199  rankeq1o  33632  finxp1o  34676  finxpreclem4  34678  finxp00  34686  aleph1min  39936  clsk1indlem1  40415