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 1570	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  38291  finxpreclem3  38316  finxpreclem4  38317  finxpsuclem  38320  finxp2o  38322  pw2f1ocnv  44043  pwfi2f1o  44097  oege2  44308  oaomoencom  44318  oaltom  44405  oe2  44406  omltoe  44407  nlim2NEW  44443  clsk1indlem1  45044