Definition df-2o 8477

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 8470	. 2 class 2o
2		c1o 8469	. . 3 class 1o
3	2	csuc 6364	. 2 class suc 1o
4	1, 3	wceq 1569	1 wff 2o = suc 1o

This definition is used by:  df2o3  8484  2on  8490  2on0  8491  ondif2  8510  o1p1e2  8548  o2p2e4  8549  oneo  8589  om2  8594  2onnALT  8652  1one2o  8655  nnm2  8662  nnneo  8664  nneob  8665  1sdom2ALT  9240  en2  9271  pm54.43  10082  en2eleq  10087  en2other2  10088  infxpenc  10097  infxpenc2  10101  dju1p1e2ALT  10253  fin1a2lem4  10481  cfpwsdom  10669  canthp1lem2  10738  pwxpndom2  10750  tsk2  10850  hash2  14549  f1otrspeq  19661  pmtrf  19669  pmtrmvd  19670  pmtrfinv  19675  efgmnvl  19928  isnzr2  20768  ltsval2  28013  nosgnn0  28015  ltssolem1  28032  nosepnelem  28036  nolt02o  28052  nogt01o  28053  bdaypw2n0bndlem  28849  unidifsnel  33131  unidifsnne  33132  r12  35726  ex-sategoelel12  36192  1oequni2o  38292  finxpreclem3  38317  finxpreclem4  38318  finxpsuclem  38321  finxp2o  38323  pw2f1ocnv  44044  pwfi2f1o  44098  oege2  44309  oaomoencom  44319  oaltom  44406  oe2  44407  omltoe  44408  nlim2NEW  44444  clsk1indlem1  45045