Definition df-2o 8440

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 8433	. 2 class 2o
2		c1o 8432	. . 3 class 1o
3	2	csuc 6350	. 2 class suc 1o
4	1, 3	wceq 1562	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8447  2on  8453  2on0  8454  ondif2  8473  o1p1e2  8511  o2p2e4  8512  oneo  8552  om2  8557  2onnALT  8615  1one2o  8618  nnm2  8625  nnneo  8627  nneob  8628  1sdom2ALT  9195  en2  9226  pm54.43  9961  en2eleq  9966  en2other2  9967  infxpenc  9976  infxpenc2  9980  dju1p1e2ALT  10133  fin1a2lem4  10362  cfpwsdom  10544  canthp1lem2  10613  pwxpndom2  10625  tsk2  10725  hash2  14420  f1otrspeq  19489  pmtrf  19497  pmtrmvd  19498  pmtrfinv  19503  efgmnvl  19756  isnzr2  20570  ltsval2  27722  nosgnn0  27724  ltssolem1  27741  nosepnelem  27745  nolt02o  27761  nogt01o  27762  bdaypw2n0bndlem  28558  unidifsnel  32736  unidifsnne  32737  r12  35395  ex-sategoelel12  35782  1oequni2o  37867  finxpreclem3  37892  finxpreclem4  37893  finxpsuclem  37896  finxp2o  37898  pw2f1ocnv  43619  pwfi2f1o  43678  oege2  43889  oaomoencom  43899  oaltom  43986  oe2  43987  omltoe  43988  nlim2NEW  44024  clsk1indlem1  44626