Definition df-2o 8523

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 8516	. 2 class 2o
2		c1o 8515	. . 3 class 1o
3	2	csuc 6397	. 2 class suc 1o
4	1, 3	wceq 1537	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8530  2on  8536  2onOLD  8537  2on0  8538  2oexOLD  8543  ondif2  8558  o1p1e2  8596  o2p2e4  8597  oneo  8637  2onnALT  8699  1one2o  8702  nnm2  8709  nnneo  8711  nneob  8712  enpr2dOLD  9116  snnen2oOLD  9290  1sdom2ALT  9304  1sdomOLD  9312  en2  9343  pm54.43  10070  en2eleq  10077  en2other2  10078  infxpenc  10087  infxpenc2  10091  dju1p1e2ALT  10244  fin1a2lem4  10472  cfpwsdom  10653  canthp1lem2  10722  pwxpndom2  10734  tsk2  10834  hash2  14454  f1otrspeq  19489  pmtrf  19497  pmtrmvd  19498  pmtrfinv  19503  efgmnvl  19756  isnzr2  20544  sltval2  27719  nosgnn0  27721  sltsolem1  27738  nosepnelem  27742  nolt02o  27758  nogt01o  27759  unidifsnel  32563  unidifsnne  32564  ex-sategoelel12  35395  1oequni2o  37334  finxpreclem3  37359  finxpreclem4  37360  finxpsuclem  37363  finxp2o  37365  pw2f1ocnv  42994  pwfi2f1o  43053  oege2  43269  oaomoencom  43279  om2  43366  oaltom  43367  oe2  43368  omltoe  43369  nlim2NEW  43405  clsk1indlem1  44007