Definition df-2o 6244

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 6237	. 2 class 2o
2		c1o 6236	. . 3 class 1o
3	2	csuc 4225	. 2 class suc 1o
4	1, 3	wceq 1299	1 wff 2o = suc 1o

This definition is referenced by:  2on  6252  2on0  6253  df2o3  6257  o1p1e2  6294  2onn  6347  nnm2  6351  snnen2og  6682  1nen2  6684  infnninf  6934  nnnninf  6935  pm54.43  6957  en2eleq  6960  en2other2  6961  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  prarloclemarch2  7128  prarloclemlt  7202  prarloclemn  7208  hash2  10399  pwle2  12779  nnsf  12783