Definition df-2o 8400

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 8393	. 2 class 2o
2		c1o 8392	. . 3 class 1o
3	2	csuc 6315	. 2 class suc 1o
4	1, 3	wceq 1548	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8407  2on  8412  2on0  8413  ondif2  8431  o1p1e2  8469  o2p2e4  8470  oneo  8510  om2  8515  2onnALT  8573  1one2o  8576  nnm2  8583  nnneo  8585  nneob  8586  1sdom2ALT  9153  en2  9184  pm54.43  9920  en2eleq  9925  en2other2  9926  infxpenc  9935  infxpenc2  9939  dju1p1e2ALT  10092  fin1a2lem4  10321  cfpwsdom  10503  canthp1lem2  10572  pwxpndom2  10584  tsk2  10684  hash2  14362  f1otrspeq  19416  pmtrf  19424  pmtrmvd  19425  pmtrfinv  19430  efgmnvl  19683  isnzr2  20493  ltsval2  27640  nosgnn0  27642  ltssolem1  27659  nosepnelem  27663  nolt02o  27679  nogt01o  27680  bdaypw2n0bndlem  28475  unidifsnel  32625  unidifsnne  32626  r12  35289  ex-sategoelel12  35668  1oequni2o  37743  finxpreclem3  37768  finxpreclem4  37769  finxpsuclem  37772  finxp2o  37774  pw2f1ocnv  43495  pwfi2f1o  43554  oege2  43765  oaomoencom  43775  oaltom  43862  oe2  43863  omltoe  43864  nlim2NEW  43900  clsk1indlem1  44502