Definition df-1o 7169

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 7162	. 2 class 1o
2		c0 3699	. . 3 class (/)
3	2	csuc 5404	. 2 class suc (/)
4	1, 3	wceq 1448	1 wff 1o = suc (/)

This definition is referenced by:  1on  7176  df1o2  7181  ordgt0ge1  7186  oa1suc  7220  om1  7230  oe1  7232  oelim2  7283  nnecl  7301  1onn  7327  omabs  7335  nnm1  7336  0sdom1dom  7757  ackbij1lem14  8650  aleph1  8983  cfpwsdom  8996  nlt1pi  9318  indpi  9319  hash1  12575  aleph1re  14308  bnj168  29544  sltval2  30549  sltsolem1  30563  rankeq1o  30944  bj-1ex  31546  finxp1o  31786  finxpreclem4  31788  finxp00  31796