Definition df-2o 4270

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 4265	. 2 class 2o
2		c1o 4264	. . 3 class 1o
3	2	csuc 2977	. 2 class suc 1o
4	1, 3	wceq 992	1 wff 2o = suc 1o

This definition is referenced by:  2on 4275  df2o2 4277  o1p1e2 4311  oneo 4348  2onn 4394  pm54.43 4715  unxpdomlem 4993  top2usne 11051

Copyright terms: Public domain