Definition df-2o 8452

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

This definition is used by:  df2o3  8459  2on  8465  2on0  8466  ondif2  8485  o1p1e2  8523  o2p2e4  8524  oneo  8564  om2  8569  2onnALT  8627  1one2o  8630  nnm2  8637  nnneo  8639  nneob  8640  1sdom2ALT  9207  en2  9238  pm54.43  9994  en2eleq  9999  en2other2  10000  infxpenc  10009  infxpenc2  10013  dju1p1e2ALT  10165  fin1a2lem4  10393  cfpwsdom  10575  canthp1lem2  10644  pwxpndom2  10656  tsk2  10756  hash2  14448  f1otrspeq  19523  pmtrf  19531  pmtrmvd  19532  pmtrfinv  19537  efgmnvl  19790  isnzr2  20626  ltsval2  27831  nosgnn0  27833  ltssolem1  27850  nosepnelem  27854  nolt02o  27870  nogt01o  27871  bdaypw2n0bndlem  28667  unidifsnel  32892  unidifsnne  32893  r12  35497  ex-sategoelel12  35927  1oequni2o  38042  finxpreclem3  38067  finxpreclem4  38068  finxpsuclem  38071  finxp2o  38073  pw2f1ocnv  43792  pwfi2f1o  43851  oege2  44062  oaomoencom  44072  oaltom  44159  oe2  44160  omltoe  44161  nlim2NEW  44197  clsk1indlem1  44799