Definition df-2o 8408

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 8401	. 2 class 2o
2		c1o 8400	. . 3 class 1o
3	2	csuc 6327	. 2 class suc 1o
4	1, 3	wceq 1542	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8415  2on  8420  2on0  8421  ondif2  8439  o1p1e2  8477  o2p2e4  8478  oneo  8518  om2  8523  2onnALT  8581  1one2o  8584  nnm2  8591  nnneo  8593  nneob  8594  1sdom2ALT  9161  en2  9192  pm54.43  9927  en2eleq  9932  en2other2  9933  infxpenc  9942  infxpenc2  9946  dju1p1e2ALT  10099  fin1a2lem4  10327  cfpwsdom  10509  canthp1lem2  10578  pwxpndom2  10590  tsk2  10690  hash2  14369  f1otrspeq  19424  pmtrf  19432  pmtrmvd  19433  pmtrfinv  19438  efgmnvl  19691  isnzr2  20497  ltsval2  27622  nosgnn0  27624  ltssolem1  27641  nosepnelem  27645  nolt02o  27661  nogt01o  27662  bdaypw2n0bndlem  28457  unidifsnel  32607  unidifsnne  32608  r12  35240  ex-sategoelel12  35611  1oequni2o  37686  finxpreclem3  37711  finxpreclem4  37712  finxpsuclem  37715  finxp2o  37717  pw2f1ocnv  43467  pwfi2f1o  43526  oege2  43737  oaomoencom  43747  oaltom  43834  oe2  43835  omltoe  43836  nlim2NEW  43872  clsk1indlem1  44474