Definition df-2o 8479

Description: Define the ordinal number 2. Lemma 3.17 of [Schloeder] p. 10. (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 8472	. 2 class 2o
2		c1o 8471	. . 3 class 1o
3	2	csuc 6354	. 2 class suc 1o
4	1, 3	wceq 1540	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8486  2on  8492  2onOLD  8493  2on0  8494  ondif2  8512  o1p1e2  8550  o2p2e4  8551  oneo  8591  2onnALT  8653  1one2o  8656  nnm2  8663  nnneo  8665  nneob  8666  enpr2dOLD  9062  snnen2oOLD  9234  1sdom2ALT  9247  1sdomOLD  9255  en2  9285  pm54.43  10013  en2eleq  10020  en2other2  10021  infxpenc  10030  infxpenc2  10034  dju1p1e2ALT  10187  fin1a2lem4  10415  cfpwsdom  10596  canthp1lem2  10665  pwxpndom2  10677  tsk2  10777  hash2  14421  f1otrspeq  19426  pmtrf  19434  pmtrmvd  19435  pmtrfinv  19440  efgmnvl  19693  isnzr2  20476  sltval2  27618  nosgnn0  27620  sltsolem1  27637  nosepnelem  27641  nolt02o  27657  nogt01o  27658  unidifsnel  32462  unidifsnne  32463  ex-sategoelel12  35395  1oequni2o  37332  finxpreclem3  37357  finxpreclem4  37358  finxpsuclem  37361  finxp2o  37363  pw2f1ocnv  43008  pwfi2f1o  43067  oege2  43278  oaomoencom  43288  om2  43375  oaltom  43376  oe2  43377  omltoe  43378  nlim2NEW  43414  clsk1indlem1  44016