Definition df-2o 8181

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 8174	. 2 class 2o
2		c1o 8173	. . 3 class 1o
3	2	csuc 6193	. 2 class suc 1o
4	1, 3	wceq 1543	1 wff 2o = suc 1o

This definition is referenced by:  2on  8188  2on0  8189  df2o3  8195  2oexOLD  8198  ondif2  8207  o1p1e2  8245  o2p2e4  8246  o2p2e4OLD  8247  oneo  8287  2onn  8346  1one2o  8349  nnm2  8356  nnneo  8358  nneob  8359  enpr2d  8703  snnen2o  8814  1sdom2  8853  1sdom  8857  en2  8888  pm54.43  9582  en2eleq  9587  en2other2  9588  infxpenc  9597  infxpenc2  9601  dju1p1e2ALT  9753  fin1a2lem4  9982  cfpwsdom  10163  canthp1lem2  10232  pwxpndom2  10244  tsk2  10344  hash2  13937  f1otrspeq  18793  pmtrf  18801  pmtrmvd  18802  pmtrfinv  18807  efgmnvl  19058  isnzr2  20255  unidifsnel  30556  unidifsnne  30557  ex-sategoelel12  33056  sltval2  33545  nosgnn0  33547  sltsolem1  33564  nosepnelem  33568  nolt02o  33584  nogt01o  33585  1oequni2o  35225  finxpreclem3  35250  finxpreclem4  35251  finxpsuclem  35254  finxp2o  35256  pw2f1ocnv  40503  pwfi2f1o  40565  clsk1indlem1  41273