Definition df-2o 4134

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 4129	. 2 class 2o
2		c1o 4128	. . 3 class 1o
3	2	csuc 2950	. 2 class suc 1o
4	1, 3	wceq 956	1 wff 2o = suc 1o

This definition is referenced by:  2on 4139  df2o2 4141  o1p1e2 4175  oneo 4212  2onn 4254  pm54.43 4572  unxpdomlem 4843  top2usne 10549

Copyright terms: Public domain