Definition df-2o 8463

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 8456	. 2 class 2o
2		c1o 8455	. . 3 class 1o
3	2	csuc 6357	. 2 class suc 1o
4	1, 3	wceq 1533	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8470  2on  8476  2onOLD  8477  2on0  8478  2oexOLD  8483  ondif2  8498  o1p1e2  8536  o2p2e4  8537  oneo  8577  2onnALT  8639  1one2o  8642  nnm2  8649  nnneo  8651  nneob  8652  enpr2dOLD  9047  snnen2oOLD  9224  1sdom2ALT  9238  1sdomOLD  9246  en2  9278  pm54.43  9993  en2eleq  10000  en2other2  10001  infxpenc  10010  infxpenc2  10014  dju1p1e2ALT  10166  fin1a2lem4  10395  cfpwsdom  10576  canthp1lem2  10645  pwxpndom2  10657  tsk2  10757  hash2  14363  f1otrspeq  19359  pmtrf  19367  pmtrmvd  19368  pmtrfinv  19373  efgmnvl  19626  isnzr2  20412  sltval2  27508  nosgnn0  27510  sltsolem1  27527  nosepnelem  27531  nolt02o  27547  nogt01o  27548  unidifsnel  32244  unidifsnne  32245  ex-sategoelel12  34909  1oequni2o  36740  finxpreclem3  36765  finxpreclem4  36766  finxpsuclem  36769  finxp2o  36771  pw2f1ocnv  42290  pwfi2f1o  42352  oege2  42571  oaomoencom  42581  om2  42669  oaltom  42670  oe2  42671  omltoe  42672  nlim2NEW  42708  clsk1indlem1  43310