Definition df-2o 6648

Description: Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.)

Assertion

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

Detailed syntax breakdown of Definition df-2o

Step	Hyp	Ref	Expression
1		c2o 6641	. 2 class 2o
2		c1o 6640	. . 3 class 1o
3	2	csuc 4486	. 2 class suc 1o
4	1, 3	wceq 1398	1 wff 2o = suc 1o

This definition is referenced by:  2on  6656  2on0  6657  df2o3  6662  o1p1e2  6701  2onn  6754  nnm2  6759  enpr2d  7064  snnen2og  7113  1nen2  7115  pm54.43  7487  en2eleq  7498  en2other2  7499  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  prarloclemarch2  7734  prarloclemlt  7808  prarloclemn  7814  hash2  11177  bj-el2oss1o  16546  pwle2  16772  nnsf  16783