Definition df-2o 8464

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 8457	. 2 class 2o
2		c1o 8456	. . 3 class 1o
3	2	csuc 6364	. 2 class suc 1o
4	1, 3	wceq 1542	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8471  2on  8477  2onOLD  8478  2on0  8479  2oexOLD  8484  ondif2  8499  o1p1e2  8537  o2p2e4  8538  oneo  8578  2onnALT  8639  1one2o  8642  nnm2  8649  nnneo  8651  nneob  8652  enpr2dOLD  9047  snnen2oOLD  9224  1sdom2ALT  9238  1sdomOLD  9246  en2  9278  pm54.43  9993  en2eleq  10000  en2other2  10001  infxpenc  10010  infxpenc2  10014  dju1p1e2ALT  10166  fin1a2lem4  10395  cfpwsdom  10576  canthp1lem2  10645  pwxpndom2  10657  tsk2  10757  hash2  14362  f1otrspeq  19310  pmtrf  19318  pmtrmvd  19319  pmtrfinv  19324  efgmnvl  19577  isnzr2  20290  sltval2  27149  nosgnn0  27151  sltsolem1  27168  nosepnelem  27172  nolt02o  27188  nogt01o  27189  unidifsnel  31760  unidifsnne  31761  ex-sategoelel12  34407  1oequni2o  36238  finxpreclem3  36263  finxpreclem4  36264  finxpsuclem  36267  finxp2o  36269  pw2f1ocnv  41762  pwfi2f1o  41824  oege2  42043  oaomoencom  42053  om2  42141  oaltom  42142  oe2  42143  omltoe  42144  nlim2NEW  42180  clsk1indlem1  42782