Definition df-2o 7561

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 7554	. 2 class 2o
2		c1o 7553	. . 3 class 1o
3	2	csuc 5725	. 2 class suc 1o
4	1, 3	wceq 1483	1 wff 2o = suc 1o

This definition is referenced by:  2on  7568  2on0  7569  df2o3  7573  ondif2  7582  o1p1e2  7620  o2p2e4  7621  oneo  7661  2onn  7720  nnm2  7729  nnneo  7731  nneob  7732  snnen2o  8149  1sdom2  8159  1sdom  8163  en2  8196  pm54.43  8826  en2eleq  8831  en2other2  8832  infxpenc  8841  infxpenc2  8845  pm110.643ALT  9000  fin1a2lem4  9225  cfpwsdom  9406  canthp1lem2  9475  pwxpndom2  9487  tsk2  9587  hash2  13193  f1otrspeq  17867  pmtrf  17875  pmtrmvd  17876  pmtrfinv  17881  efgmnvl  18127  isnzr2  19263  sltval2  31809  nosgnn0  31811  sltsolem1  31826  nosepnelem  31830  nolt02o  31845  bj-2ex  32939  1oequni2o  33216  finxpreclem3  33230  finxpreclem4  33231  finxpsuclem  33234  finxp2o  33236  pw2f1ocnv  37604  pwfi2f1o  37666  clsk1indlem1  38343