Definition df-2o 6475

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 6468	. 2 class 2o
2		c1o 6467	. . 3 class 1o
3	2	csuc 4400	. 2 class suc 1o
4	1, 3	wceq 1364	1 wff 2o = suc 1o

This definition is referenced by:  2on  6483  2on0  6484  df2o3  6488  o1p1e2  6526  2onn  6579  nnm2  6584  enpr2d  6876  snnen2og  6920  1nen2  6922  pm54.43  7257  en2eleq  7262  en2other2  7263  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  prarloclemarch2  7486  prarloclemlt  7560  prarloclemn  7566  hash2  10904  bj-el2oss1o  15420  pwle2  15643  nnsf  15649