Definition df-2o 6583

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 6576	. 2 class 2o
2		c1o 6575	. . 3 class 1o
3	2	csuc 4462	. 2 class suc 1o
4	1, 3	wceq 1397	1 wff 2o = suc 1o

This definition is referenced by:  2on  6591  2on0  6592  df2o3  6597  o1p1e2  6636  2onn  6689  nnm2  6694  enpr2d  6997  snnen2og  7045  1nen2  7047  pm54.43  7395  en2eleq  7406  en2other2  7407  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  prarloclemarch2  7639  prarloclemlt  7713  prarloclemn  7719  hash2  11077  bj-el2oss1o  16421  pwle2  16650  nnsf  16658