Definition df-2o 6582

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 6575	. 2 class 2o
2		c1o 6574	. . 3 class 1o
3	2	csuc 4462	. 2 class suc 1o
4	1, 3	wceq 1397	1 wff 2o = suc 1o

This definition is referenced by:  2on  6590  2on0  6591  df2o3  6596  o1p1e2  6635  2onn  6688  nnm2  6693  enpr2d  6996  snnen2og  7044  1nen2  7046  pm54.43  7394  en2eleq  7405  en2other2  7406  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  prarloclemarch2  7638  prarloclemlt  7712  prarloclemn  7718  hash2  11075  bj-el2oss1o  16370  pwle2  16599  nnsf  16607