Definition df-2o 6314

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 6307	. 2 class 2o
2		c1o 6306	. . 3 class 1o
3	2	csuc 4287	. 2 class suc 1o
4	1, 3	wceq 1331	1 wff 2o = suc 1o

This definition is referenced by:  2on  6322  2on0  6323  df2o3  6327  o1p1e2  6364  2onn  6417  nnm2  6421  enpr2d  6711  snnen2og  6753  1nen2  6755  infnninf  7022  nnnninf  7023  pm54.43  7046  en2eleq  7051  en2other2  7052  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  prarloclemarch2  7227  prarloclemlt  7301  prarloclemn  7307  hash2  10558  bj-el2oss1o  12981  pwle2  13193  nnsf  13199