Definition df-2o 6472

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 6465	. 2 class 2o
2		c1o 6464	. . 3 class 1o
3	2	csuc 4397	. 2 class suc 1o
4	1, 3	wceq 1364	1 wff 2o = suc 1o

This definition is referenced by:  2on  6480  2on0  6481  df2o3  6485  o1p1e2  6523  2onn  6576  nnm2  6581  enpr2d  6873  snnen2og  6917  1nen2  6919  pm54.43  7252  en2eleq  7257  en2other2  7258  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  prarloclemarch2  7481  prarloclemlt  7555  prarloclemn  7561  hash2  10886  bj-el2oss1o  15336  pwle2  15559  nnsf  15565