Definition df-2o 5178

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 5173	. 2 class 2o
2		c1o 5172	. . 3 class 1o
3	2	csuc 3659	. 2 class suc 1o
4	1, 3	wceq 1298	1 wff 2o = suc 1o

This definition is referenced by:  2on 5183  2onOLD 5184  df2o2 5186  o1p1e2 5222  oneo 5260  2onn 5311  pm54.43 5662  unxpdomlem 5995  2on0 13862  sltval2 13997  nosgnn0 13999  axsltsolem1 14006  top2usne 14898

Copyright terms: Public domain