Definition df-2o 8410

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 8403	. 2 class 2o
2		c1o 8402	. . 3 class 1o
3	2	csuc 6329	. 2 class suc 1o
4	1, 3	wceq 1542	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8417  2on  8422  2on0  8423  ondif2  8441  o1p1e2  8479  o2p2e4  8480  oneo  8520  om2  8525  2onnALT  8583  1one2o  8586  nnm2  8593  nnneo  8595  nneob  8596  1sdom2ALT  9163  en2  9194  pm54.43  9927  en2eleq  9932  en2other2  9933  infxpenc  9942  infxpenc2  9946  dju1p1e2ALT  10099  fin1a2lem4  10327  cfpwsdom  10509  canthp1lem2  10578  pwxpndom2  10590  tsk2  10690  hash2  14342  f1otrspeq  19393  pmtrf  19401  pmtrmvd  19402  pmtrfinv  19407  efgmnvl  19660  isnzr2  20468  ltsval2  27641  nosgnn0  27643  ltssolem1  27660  nosepnelem  27664  nolt02o  27680  nogt01o  27681  bdaypw2n0bndlem  28476  unidifsnel  32628  unidifsnne  32629  r12  35278  ex-sategoelel12  35649  1oequni2o  37650  finxpreclem3  37675  finxpreclem4  37676  finxpsuclem  37679  finxp2o  37681  pw2f1ocnv  43423  pwfi2f1o  43482  oege2  43693  oaomoencom  43703  oaltom  43790  oe2  43791  omltoe  43792  nlim2NEW  43828  clsk1indlem1  44430