Definition df-1o 3104

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 3099	. 2 class 1o
2		c0 1707	. . 3 class (/)
3	2	csuc 2201	. 2 class suc (/)
4	1, 3	wceq 1091	1 wff 1o = suc (/)

This definition is referenced by:  1o 3109  df1o2 3111  ordgt0ge1 3114  oa1suc 3132  om1 3144  oe1 3146  1onn 3193  0sdom1dom 3420  aleph1 3676  1pi 3805  1lt2pi 3826  nlt1pi 3827  indpi 3828

metamath.org