Definition df-2o 6268

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 6261	. 2 class 2o
2		c1o 6260	. . 3 class 1o
3	2	csuc 4247	. 2 class suc 1o
4	1, 3	wceq 1314	1 wff 2o = suc 1o

This definition is referenced by:  2on  6276  2on0  6277  df2o3  6281  o1p1e2  6318  2onn  6371  nnm2  6375  snnen2og  6706  1nen2  6708  infnninf  6972  nnnninf  6973  pm54.43  6996  en2eleq  6999  en2other2  7000  exmidfodomrlemr  7006  exmidfodomrlemrALT  7007  prarloclemarch2  7175  prarloclemlt  7249  prarloclemn  7255  hash2  10451  pwle2  12885  nnsf  12891