Definition df-2o 8455

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 8448	. 2 class 2o
2		c1o 8447	. . 3 class 1o
3	2	csuc 6353	. 2 class suc 1o
4	1, 3	wceq 1570	1 wff 2o = suc 1o

This definition is used by:  df2o3  8462  2on  8468  2on0  8469  ondif2  8488  o1p1e2  8526  o2p2e4  8527  oneo  8567  om2  8572  2onnALT  8630  1one2o  8633  nnm2  8640  nnneo  8642  nneob  8643  1sdom2ALT  9218  en2  9249  pm54.43  10053  en2eleq  10058  en2other2  10059  infxpenc  10068  infxpenc2  10072  dju1p1e2ALT  10224  fin1a2lem4  10452  cfpwsdom  10640  canthp1lem2  10709  pwxpndom2  10721  tsk2  10821  hash2  14516  f1otrspeq  19622  pmtrf  19630  pmtrmvd  19631  pmtrfinv  19636  efgmnvl  19889  isnzr2  20729  ltsval2  27946  nosgnn0  27948  ltssolem1  27965  nosepnelem  27969  nolt02o  27985  nogt01o  27986  bdaypw2n0bndlem  28782  unidifsnel  33064  unidifsnne  33065  r12  35656  ex-sategoelel12  36113  1oequni2o  38211  finxpreclem3  38236  finxpreclem4  38237  finxpsuclem  38240  finxp2o  38242  pw2f1ocnv  43982  pwfi2f1o  44041  oege2  44252  oaomoencom  44262  oaltom  44349  oe2  44350  omltoe  44351  nlim2NEW  44387  clsk1indlem1  44989