Definition df-1o 7048

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 7041	. 2 class 1o
2		c0 3711	. . 3 class (/)
3	2	csuc 4794	. 2 class suc (/)
4	1, 3	wceq 1399	1 wff 1o = suc (/)

This definition is referenced by:  1on  7055  df1o2  7060  ordgt0ge1  7065  oa1suc  7099  om1  7109  oe1  7111  oelim2  7162  nnecl  7180  1onn  7206  omabs  7214  nnm1  7215  0sdom1dom  7634  ackbij1lem14  8526  aleph1  8859  cfpwsdom  8872  nlt1pi  9195  indpi  9196  hash1  12373  aleph1re  13980  sltval2  29581  sltsolem1  29593  rankeq1o  29981  bnj168  34132  bj-1ex  34855