Definition df-1o 4269

Description: Define the ordinal number 1.

Assertion

Ref	Expression
df-1o	|- 1o = suc (/)

Detailed syntax breakdown of Definition df-1o

Step	Hyp	Ref	Expression
1		c1o 4264	. 2 class 1o
2		c0 2332	. . 3 class (/)
3	2	csuc 2977	. 2 class suc (/)
4	1, 3	wceq 992	1 wff 1o = suc (/)

This definition is referenced by:  1on 4274  df1o2 4276  ordgt0ge1 4280  oa1suc 4300  om1 4312  oe1 4314  oelim2 4358  nnecl 4371  1onn 4393  0sdom1dom 4671  aleph1 5021  nlt1pi 5187  indpi 5188  aleph1re 7763  top2usne 11051

Copyright terms: Public domain