Definition df-2o 8438

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 8431	. 2 class 2o
2		c1o 8430	. . 3 class 1o
3	2	csuc 6337	. 2 class suc 1o
4	1, 3	wceq 1540	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8445  2on  8450  2on0  8451  ondif2  8469  o1p1e2  8507  o2p2e4  8508  oneo  8548  2onnALT  8610  1one2o  8613  nnm2  8620  nnneo  8622  nneob  8623  enpr2dOLD  9024  1sdom2ALT  9195  1sdomOLD  9203  en2  9233  pm54.43  9961  en2eleq  9968  en2other2  9969  infxpenc  9978  infxpenc2  9982  dju1p1e2ALT  10135  fin1a2lem4  10363  cfpwsdom  10544  canthp1lem2  10613  pwxpndom2  10625  tsk2  10725  hash2  14377  f1otrspeq  19384  pmtrf  19392  pmtrmvd  19393  pmtrfinv  19398  efgmnvl  19651  isnzr2  20434  sltval2  27575  nosgnn0  27577  sltsolem1  27594  nosepnelem  27598  nolt02o  27614  nogt01o  27615  unidifsnel  32471  unidifsnne  32472  ex-sategoelel12  35421  1oequni2o  37363  finxpreclem3  37388  finxpreclem4  37389  finxpsuclem  37392  finxp2o  37394  pw2f1ocnv  43033  pwfi2f1o  43092  oege2  43303  oaomoencom  43313  om2  43400  oaltom  43401  oe2  43402  omltoe  43403  nlim2NEW  43439  clsk1indlem1  44041