Definition df-2o 8507

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 8500	. 2 class 2o
2		c1o 8499	. . 3 class 1o
3	2	csuc 6386	. 2 class suc 1o
4	1, 3	wceq 1540	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8514  2on  8520  2onOLD  8521  2on0  8522  ondif2  8540  o1p1e2  8578  o2p2e4  8579  oneo  8619  2onnALT  8681  1one2o  8684  nnm2  8691  nnneo  8693  nneob  8694  enpr2dOLD  9090  snnen2oOLD  9264  1sdom2ALT  9277  1sdomOLD  9285  en2  9315  pm54.43  10041  en2eleq  10048  en2other2  10049  infxpenc  10058  infxpenc2  10062  dju1p1e2ALT  10215  fin1a2lem4  10443  cfpwsdom  10624  canthp1lem2  10693  pwxpndom2  10705  tsk2  10805  hash2  14444  f1otrspeq  19465  pmtrf  19473  pmtrmvd  19474  pmtrfinv  19479  efgmnvl  19732  isnzr2  20518  sltval2  27701  nosgnn0  27703  sltsolem1  27720  nosepnelem  27724  nolt02o  27740  nogt01o  27741  unidifsnel  32553  unidifsnne  32554  ex-sategoelel12  35432  1oequni2o  37369  finxpreclem3  37394  finxpreclem4  37395  finxpsuclem  37398  finxp2o  37400  pw2f1ocnv  43049  pwfi2f1o  43108  oege2  43320  oaomoencom  43330  om2  43417  oaltom  43418  oe2  43419  omltoe  43420  nlim2NEW  43456  clsk1indlem1  44058