Definition df-2o 8467

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 8460	. 2 class 2o
2		c1o 8459	. . 3 class 1o
3	2	csuc 6367	. 2 class suc 1o
4	1, 3	wceq 1542	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8474  2on  8480  2onOLD  8481  2on0  8482  2oexOLD  8487  ondif2  8502  o1p1e2  8540  o2p2e4  8541  oneo  8581  2onnALT  8642  1one2o  8645  nnm2  8652  nnneo  8654  nneob  8655  enpr2dOLD  9050  snnen2oOLD  9227  1sdom2ALT  9241  1sdomOLD  9249  en2  9281  pm54.43  9996  en2eleq  10003  en2other2  10004  infxpenc  10013  infxpenc2  10017  dju1p1e2ALT  10169  fin1a2lem4  10398  cfpwsdom  10579  canthp1lem2  10648  pwxpndom2  10660  tsk2  10760  hash2  14365  f1otrspeq  19315  pmtrf  19323  pmtrmvd  19324  pmtrfinv  19329  efgmnvl  19582  isnzr2  20297  sltval2  27159  nosgnn0  27161  sltsolem1  27178  nosepnelem  27182  nolt02o  27198  nogt01o  27199  unidifsnel  31772  unidifsnne  31773  ex-sategoelel12  34418  1oequni2o  36249  finxpreclem3  36274  finxpreclem4  36275  finxpsuclem  36278  finxp2o  36280  pw2f1ocnv  41776  pwfi2f1o  41838  oege2  42057  oaomoencom  42067  om2  42155  oaltom  42156  oe2  42157  omltoe  42158  nlim2NEW  42194  clsk1indlem1  42796