Definition df-2o 8389

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 8382	. 2 class 2o
2		c1o 8381	. . 3 class 1o
3	2	csuc 6309	. 2 class suc 1o
4	1, 3	wceq 1540	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8396  2on  8401  2on0  8402  ondif2  8420  o1p1e2  8458  o2p2e4  8459  oneo  8499  2onnALT  8561  1one2o  8564  nnm2  8571  nnneo  8573  nneob  8574  1sdom2ALT  9138  en2  9169  pm54.43  9897  en2eleq  9902  en2other2  9903  infxpenc  9912  infxpenc2  9916  dju1p1e2ALT  10069  fin1a2lem4  10297  cfpwsdom  10478  canthp1lem2  10547  pwxpndom2  10559  tsk2  10659  hash2  14312  f1otrspeq  19326  pmtrf  19334  pmtrmvd  19335  pmtrfinv  19340  efgmnvl  19593  isnzr2  20403  sltval2  27566  nosgnn0  27568  sltsolem1  27585  nosepnelem  27589  nolt02o  27605  nogt01o  27606  unidifsnel  32479  unidifsnne  32480  ex-sategoelel12  35410  1oequni2o  37352  finxpreclem3  37377  finxpreclem4  37378  finxpsuclem  37381  finxp2o  37383  pw2f1ocnv  43020  pwfi2f1o  43079  oege2  43290  oaomoencom  43300  om2  43387  oaltom  43388  oe2  43389  omltoe  43390  nlim2NEW  43426  clsk1indlem1  44028