Definition df-2o 6470

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 6463	. 2 class 2o
2		c1o 6462	. . 3 class 1o
3	2	csuc 4396	. 2 class suc 1o
4	1, 3	wceq 1364	1 wff 2o = suc 1o

This definition is referenced by:  2on  6478  2on0  6479  df2o3  6483  o1p1e2  6521  2onn  6574  nnm2  6579  enpr2d  6871  snnen2og  6915  1nen2  6917  pm54.43  7250  en2eleq  7255  en2other2  7256  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  prarloclemarch2  7479  prarloclemlt  7553  prarloclemn  7559  hash2  10883  bj-el2oss1o  15266  pwle2  15489  nnsf  15495