Definition df-1o 6912

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 6905	. 2 class 1o
2		c0 3632	. . 3 class (/)
3	2	csuc 4716	. 2 class suc (/)
4	1, 3	wceq 1369	1 wff 1o = suc (/)

This definition is referenced by:  1on  6919  df1o2  6924  ordgt0ge1  6929  oa1suc  6963  om1  6973  oe1  6975  oelim2  7026  nnecl  7044  1onn  7070  omabs  7078  nnm1  7079  0sdom1dom  7502  ackbij1lem14  8394  aleph1  8727  cfpwsdom  8740  nlt1pi  9067  indpi  9068  hash1  12154  aleph1re  13519  sltval2  27766  sltsolem1  27778  rankeq1o  28178  bnj168  31650  bj-1ex  32342