Definition df-2o 6563

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 6556	. 2 class 2o
2		c1o 6555	. . 3 class 1o
3	2	csuc 4456	. 2 class suc 1o
4	1, 3	wceq 1395	1 wff 2o = suc 1o

This definition is referenced by:  2on  6571  2on0  6572  df2o3  6576  o1p1e2  6614  2onn  6667  nnm2  6672  enpr2d  6972  snnen2og  7020  1nen2  7022  pm54.43  7363  en2eleq  7373  en2other2  7374  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  prarloclemarch2  7606  prarloclemlt  7680  prarloclemn  7686  hash2  11034  bj-el2oss1o  16138  pwle2  16364  nnsf  16371