Definition df-2o 3105

Description: Define the ordinal number 2.

Assertion

Ref	Expression
df-2o	|- 2o = suc 1o

Detailed syntax breakdown of Definition df-2o

Step	Hyp	Ref	Expression
1		c2o 3100	. 2 class 2o
2		c1o 3099	. . 3 class 1o
3	2	csuc 2201	. 2 class suc 1o
4	1, 3	wceq 1091	1 wff 2o = suc 1o

This definition is referenced by:  2o 3110  df2o2 3112  o1p1e2 3143  2onn 3194  unxpdomlem 3649

metamath.org