Definition df-2o 8459

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 8452	. 2 class 2o
2		c1o 8451	. . 3 class 1o
3	2	csuc 6363	. 2 class suc 1o
4	1, 3	wceq 1570	1 wff 2o = suc 1o

This definition is used by:  df2o3  8466  2on  8472  2on0  8473  ondif2  8492  o1p1e2  8530  o2p2e4  8531  oneo  8571  om2  8576  2onnALT  8634  1one2o  8637  nnm2  8644  nnneo  8646  nneob  8647  1sdom2ALT  9222  en2  9253  pm54.43  10009  en2eleq  10014  en2other2  10015  infxpenc  10024  infxpenc2  10028  dju1p1e2ALT  10180  fin1a2lem4  10408  cfpwsdom  10596  canthp1lem2  10665  pwxpndom2  10677  tsk2  10777  hash2  14471  f1otrspeq  19575  pmtrf  19583  pmtrmvd  19584  pmtrfinv  19589  efgmnvl  19842  isnzr2  20679  ltsval2  27890  nosgnn0  27892  ltssolem1  27909  nosepnelem  27913  nolt02o  27929  nogt01o  27930  bdaypw2n0bndlem  28726  unidifsnel  32996  unidifsnne  32997  r12  35589  ex-sategoelel12  35993  1oequni2o  38109  finxpreclem3  38134  finxpreclem4  38135  finxpsuclem  38138  finxp2o  38140  pw2f1ocnv  43865  pwfi2f1o  43924  oege2  44135  oaomoencom  44145  oaltom  44232  oe2  44233  omltoe  44234  nlim2NEW  44270  clsk1indlem1  44872