Definition df-2o 8412

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 8405	. 2 class 2o
2		c1o 8404	. . 3 class 1o
3	2	csuc 6322	. 2 class suc 1o
4	1, 3	wceq 1540	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8419  2on  8424  2on0  8425  ondif2  8443  o1p1e2  8481  o2p2e4  8482  oneo  8522  2onnALT  8584  1one2o  8587  nnm2  8594  nnneo  8596  nneob  8597  enpr2dOLD  8998  1sdom2ALT  9165  1sdomOLD  9172  en2  9202  pm54.43  9930  en2eleq  9937  en2other2  9938  infxpenc  9947  infxpenc2  9951  dju1p1e2ALT  10104  fin1a2lem4  10332  cfpwsdom  10513  canthp1lem2  10582  pwxpndom2  10594  tsk2  10694  hash2  14346  f1otrspeq  19353  pmtrf  19361  pmtrmvd  19362  pmtrfinv  19367  efgmnvl  19620  isnzr2  20403  sltval2  27544  nosgnn0  27546  sltsolem1  27563  nosepnelem  27567  nolt02o  27583  nogt01o  27584  unidifsnel  32437  unidifsnne  32438  ex-sategoelel12  35387  1oequni2o  37329  finxpreclem3  37354  finxpreclem4  37355  finxpsuclem  37358  finxp2o  37360  pw2f1ocnv  42999  pwfi2f1o  43058  oege2  43269  oaomoencom  43279  om2  43366  oaltom  43367  oe2  43368  omltoe  43369  nlim2NEW  43405  clsk1indlem1  44007