Definition df-2o 8395

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 8388	. 2 class 2o
2		c1o 8387	. . 3 class 1o
3	2	csuc 6314	. 2 class suc 1o
4	1, 3	wceq 1542	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8402  2on  8407  2on0  8408  ondif2  8426  o1p1e2  8464  o2p2e4  8465  oneo  8505  om2  8510  2onnALT  8568  1one2o  8571  nnm2  8578  nnneo  8580  nneob  8581  1sdom2ALT  9148  en2  9179  pm54.43  9914  en2eleq  9919  en2other2  9920  infxpenc  9929  infxpenc2  9933  dju1p1e2ALT  10086  fin1a2lem4  10314  cfpwsdom  10496  canthp1lem2  10565  pwxpndom2  10577  tsk2  10677  hash2  14356  f1otrspeq  19411  pmtrf  19419  pmtrmvd  19420  pmtrfinv  19425  efgmnvl  19678  isnzr2  20484  ltsval2  27608  nosgnn0  27610  ltssolem1  27627  nosepnelem  27631  nolt02o  27647  nogt01o  27648  bdaypw2n0bndlem  28443  unidifsnel  32593  unidifsnne  32594  r12  35226  ex-sategoelel12  35597  1oequni2o  37672  finxpreclem3  37697  finxpreclem4  37698  finxpsuclem  37701  finxp2o  37703  pw2f1ocnv  43453  pwfi2f1o  43512  oege2  43723  oaomoencom  43733  oaltom  43820  oe2  43821  omltoe  43822  nlim2NEW  43858  clsk1indlem1  44460