Definition df-1o 7130

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 7123	. 2 class 1o
2		c0 3785	. . 3 class (/)
3	2	csuc 4880	. 2 class suc (/)
4	1, 3	wceq 1379	1 wff 1o = suc (/)

This definition is referenced by:  1on  7137  df1o2  7142  ordgt0ge1  7147  oa1suc  7181  om1  7191  oe1  7193  oelim2  7244  nnecl  7262  1onn  7288  omabs  7296  nnm1  7297  0sdom1dom  7717  ackbij1lem14  8613  aleph1  8946  cfpwsdom  8959  nlt1pi  9284  indpi  9285  hash1  12435  aleph1re  13839  sltval2  29021  sltsolem1  29033  rankeq1o  29433  bnj168  32883  bj-1ex  33606