Definition df-2o 8396

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 8389	. 2 class 2o
2		c1o 8388	. . 3 class 1o
3	2	csuc 6317	. 2 class suc 1o
4	1, 3	wceq 1541	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8403  2on  8408  2on0  8409  ondif2  8427  o1p1e2  8465  o2p2e4  8466  oneo  8506  om2  8511  2onnALT  8569  1one2o  8572  nnm2  8579  nnneo  8581  nneob  8582  1sdom2ALT  9147  en2  9178  pm54.43  9911  en2eleq  9916  en2other2  9917  infxpenc  9926  infxpenc2  9930  dju1p1e2ALT  10083  fin1a2lem4  10311  cfpwsdom  10493  canthp1lem2  10562  pwxpndom2  10574  tsk2  10674  hash2  14326  f1otrspeq  19374  pmtrf  19382  pmtrmvd  19383  pmtrfinv  19388  efgmnvl  19641  isnzr2  20449  sltval2  27622  nosgnn0  27624  sltsolem1  27641  nosepnelem  27645  nolt02o  27661  nogt01o  27662  bdaypw2n0s  28420  unidifsnel  32559  unidifsnne  32560  r12  35200  ex-sategoelel12  35570  1oequni2o  37512  finxpreclem3  37537  finxpreclem4  37538  finxpsuclem  37541  finxp2o  37543  pw2f1ocnv  43221  pwfi2f1o  43280  oege2  43491  oaomoencom  43501  oaltom  43588  oe2  43589  omltoe  43590  nlim2NEW  43626  clsk1indlem1  44228