Definition df-2o 8502

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 8495	. 2 class 2o
2		c1o 8494	. . 3 class 1o
3	2	csuc 6379	. 2 class suc 1o
4	1, 3	wceq 1570	1 wff 2o = suc 1o

This definition is used by:  df2o3  8509  2on  8515  2on0  8516  ondif2  8535  o1p1e2  8573  o2p2e4  8574  oneo  8614  om2  8619  2onnALT  8677  1one2o  8680  nnm2  8687  nnneo  8689  nneob  8690  1sdom2ALT  9265  en2  9296  pm54.43  10106  en2eleq  10111  en2other2  10112  infxpenc  10121  infxpenc2  10125  dju1p1e2ALT  10277  fin1a2lem4  10505  cfpwsdom  10693  canthp1lem2  10762  pwxpndom2  10774  tsk2  10874  hash2  14573  f1otrspeq  19688  pmtrf  19696  pmtrmvd  19697  pmtrfinv  19702  efgmnvl  19955  isnzr2  20795  ltsval2  28040  nosgnn0  28042  ltssolem1  28059  nosepnelem  28063  nolt02o  28079  nogt01o  28080  bdaypw2n0bndlem  28876  unidifsnel  33200  unidifsnne  33201  r12  35807  1olt9o  35879  gdlopcfv2  35972  gdlopcfv3  35973  gdlopcfv4  35974  gdlopcfv5  35975  gdlopcfv6  35976  gdlopcfv7  35977  gdlopcfv8  35978  ex-sategoelel12  36358  1oequni2o  38482  finxpreclem3  38507  finxpreclem4  38508  finxpsuclem  38511  finxp2o  38513  pw2f1ocnv  44235  pwfi2f1o  44289  oege2  44499  oaomoencom  44509  oaltom  44596  oe2  44597  omltoe  44598  nlim2NEW  44634  clsk1indlem1  45235