Definition df-2o 8400

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 8393	. 2 class 2o
2		c1o 8392	. . 3 class 1o
3	2	csuc 6320	. 2 class suc 1o
4	1, 3	wceq 1542	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8407  2on  8412  2on0  8413  ondif2  8431  o1p1e2  8469  o2p2e4  8470  oneo  8510  om2  8515  2onnALT  8573  1one2o  8576  nnm2  8583  nnneo  8585  nneob  8586  1sdom2ALT  9153  en2  9184  pm54.43  9917  en2eleq  9922  en2other2  9923  infxpenc  9932  infxpenc2  9936  dju1p1e2ALT  10089  fin1a2lem4  10317  cfpwsdom  10499  canthp1lem2  10568  pwxpndom2  10580  tsk2  10680  hash2  14332  f1otrspeq  19380  pmtrf  19388  pmtrmvd  19389  pmtrfinv  19394  efgmnvl  19647  isnzr2  20455  ltsval2  27628  nosgnn0  27630  ltssolem1  27647  nosepnelem  27651  nolt02o  27667  nogt01o  27668  bdaypw2n0bndlem  28463  unidifsnel  32613  unidifsnne  32614  r12  35253  ex-sategoelel12  35623  1oequni2o  37575  finxpreclem3  37600  finxpreclem4  37601  finxpsuclem  37604  finxp2o  37606  pw2f1ocnv  43346  pwfi2f1o  43405  oege2  43616  oaomoencom  43626  oaltom  43713  oe2  43714  omltoe  43715  nlim2NEW  43751  clsk1indlem1  44353