Definition df-2o 6493

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 6486	. 2 class 2o
2		c1o 6485	. . 3 class 1o
3	2	csuc 4410	. 2 class suc 1o
4	1, 3	wceq 1372	1 wff 2o = suc 1o

This definition is referenced by:  2on  6501  2on0  6502  df2o3  6506  o1p1e2  6544  2onn  6597  nnm2  6602  enpr2d  6894  snnen2og  6938  1nen2  6940  pm54.43  7280  en2eleq  7285  en2other2  7286  exmidfodomrlemr  7292  exmidfodomrlemrALT  7293  prarloclemarch2  7514  prarloclemlt  7588  prarloclemn  7594  hash2  10938  bj-el2oss1o  15574  pwle2  15799  nnsf  15806