Definition df-2o 8386

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 8379	. 2 class 2o
2		c1o 8378	. . 3 class 1o
3	2	csuc 6308	. 2 class suc 1o
4	1, 3	wceq 1541	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8393  2on  8398  2on0  8399  ondif2  8417  o1p1e2  8455  o2p2e4  8456  oneo  8496  2onnALT  8558  1one2o  8561  nnm2  8568  nnneo  8570  nneob  8571  1sdom2ALT  9133  en2  9164  pm54.43  9894  en2eleq  9899  en2other2  9900  infxpenc  9909  infxpenc2  9913  dju1p1e2ALT  10066  fin1a2lem4  10294  cfpwsdom  10475  canthp1lem2  10544  pwxpndom2  10556  tsk2  10656  hash2  14312  f1otrspeq  19359  pmtrf  19367  pmtrmvd  19368  pmtrfinv  19373  efgmnvl  19626  isnzr2  20433  sltval2  27595  nosgnn0  27597  sltsolem1  27614  nosepnelem  27618  nolt02o  27634  nogt01o  27635  unidifsnel  32515  unidifsnne  32516  r12  35106  ex-sategoelel12  35471  1oequni2o  37412  finxpreclem3  37437  finxpreclem4  37438  finxpsuclem  37441  finxp2o  37443  pw2f1ocnv  43140  pwfi2f1o  43199  oege2  43410  oaomoencom  43420  om2  43507  oaltom  43508  oe2  43509  omltoe  43510  nlim2NEW  43546  clsk1indlem1  44148