Definition df-2o 8403

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 8396	. 2 class 2o
2		c1o 8395	. . 3 class 1o
3	2	csuc 6323	. 2 class suc 1o
4	1, 3	wceq 1542	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8410  2on  8415  2on0  8416  ondif2  8434  o1p1e2  8472  o2p2e4  8473  oneo  8513  om2  8518  2onnALT  8576  1one2o  8579  nnm2  8586  nnneo  8588  nneob  8589  1sdom2ALT  9156  en2  9187  pm54.43  9922  en2eleq  9927  en2other2  9928  infxpenc  9937  infxpenc2  9941  dju1p1e2ALT  10094  fin1a2lem4  10322  cfpwsdom  10504  canthp1lem2  10573  pwxpndom2  10585  tsk2  10685  hash2  14364  f1otrspeq  19419  pmtrf  19427  pmtrmvd  19428  pmtrfinv  19433  efgmnvl  19686  isnzr2  20492  ltsval2  27617  nosgnn0  27619  ltssolem1  27636  nosepnelem  27640  nolt02o  27656  nogt01o  27657  bdaypw2n0bndlem  28452  unidifsnel  32602  unidifsnne  32603  r12  35235  ex-sategoelel12  35606  1oequni2o  37681  finxpreclem3  37706  finxpreclem4  37707  finxpsuclem  37710  finxp2o  37712  pw2f1ocnv  43462  pwfi2f1o  43521  oege2  43732  oaomoencom  43742  oaltom  43829  oe2  43830  omltoe  43831  nlim2NEW  43867  clsk1indlem1  44469