Definition df-1o 4133

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 4128	. 2 class 1o
2		c0 2280	. . 3 class (/)
3	2	csuc 2950	. 2 class suc (/)
4	1, 3	wceq 956	1 wff 1o = suc (/)

This definition is referenced by:  1on 4138  df1o2 4140  ordgt0ge1 4144  oa1suc 4164  om1 4176  oe1 4178  oelim2 4222  nnecl 4231  1onn 4253  0sdom1dom 4525  aleph1 4871  nlt1pi 5033  indpi 5034  aleph1re 7551  top2usne 10549

Copyright terms: Public domain