Definition df-2o 6376

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 6369	. 2 class 2o
2		c1o 6368	. . 3 class 1o
3	2	csuc 4337	. 2 class suc 1o
4	1, 3	wceq 1342	1 wff 2o = suc 1o

This definition is referenced by:  2on  6384  2on0  6385  df2o3  6389  o1p1e2  6427  2onn  6480  nnm2  6484  enpr2d  6774  snnen2og  6816  1nen2  6818  pm54.43  7137  en2eleq  7142  en2other2  7143  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  prarloclemarch2  7351  prarloclemlt  7425  prarloclemn  7431  hash2  10714  bj-el2oss1o  13490  pwle2  13712  nnsf  13719