Definition df-2o 8453

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 8446	. 2 class 2o
2		c1o 8445	. . 3 class 1o
3	2	csuc 6362	. 2 class suc 1o
4	1, 3	wceq 1568	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8460  2on  8466  2on0  8467  ondif2  8486  o1p1e2  8524  o2p2e4  8525  oneo  8565  om2  8570  2onnALT  8628  1one2o  8631  nnm2  8638  nnneo  8640  nneob  8641  1sdom2ALT  9208  en2  9239  pm54.43  9986  en2eleq  9991  en2other2  9992  infxpenc  10001  infxpenc2  10005  dju1p1e2ALT  10157  fin1a2lem4  10386  cfpwsdom  10568  canthp1lem2  10637  pwxpndom2  10649  tsk2  10749  hash2  14440  f1otrspeq  19516  pmtrf  19524  pmtrmvd  19525  pmtrfinv  19530  efgmnvl  19783  isnzr2  20600  ltsval2  27796  nosgnn0  27798  ltssolem1  27815  nosepnelem  27819  nolt02o  27835  nogt01o  27836  bdaypw2n0bndlem  28632  unidifsnel  32847  unidifsnne  32848  r12  35452  ex-sategoelel12  35873  1oequni2o  37958  finxpreclem3  37983  finxpreclem4  37984  finxpsuclem  37987  finxp2o  37989  pw2f1ocnv  43712  pwfi2f1o  43771  oege2  43982  oaomoencom  43992  oaltom  44079  oe2  44080  omltoe  44081  nlim2NEW  44117  clsk1indlem1  44719