Definition df-2o 8268

Description: Define the ordinal number 2. (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 8261	. 2 class 2o
2		c1o 8260	. . 3 class 1o
3	2	csuc 6253	. 2 class suc 1o
4	1, 3	wceq 1539	1 wff 2o = suc 1o

This definition is referenced by:  2on  8275  2on0  8276  df2o3  8282  2oexOLD  8285  ondif2  8294  o1p1e2  8332  o2p2e4  8333  o2p2e4OLD  8334  oneo  8374  2onn  8433  1one2o  8436  nnm2  8443  nnneo  8445  nneob  8446  enpr2d  8792  snnen2o  8903  1sdom2  8951  1sdom  8955  en2  8983  pm54.43  9690  en2eleq  9695  en2other2  9696  infxpenc  9705  infxpenc2  9709  dju1p1e2ALT  9861  fin1a2lem4  10090  cfpwsdom  10271  canthp1lem2  10340  pwxpndom2  10352  tsk2  10452  hash2  14048  f1otrspeq  18970  pmtrf  18978  pmtrmvd  18979  pmtrfinv  18984  efgmnvl  19235  isnzr2  20447  unidifsnel  30784  unidifsnne  30785  ex-sategoelel12  33289  sltval2  33786  nosgnn0  33788  sltsolem1  33805  nosepnelem  33809  nolt02o  33825  nogt01o  33826  1oequni2o  35466  finxpreclem3  35491  finxpreclem4  35492  finxpsuclem  35495  finxp2o  35497  pw2f1ocnv  40775  pwfi2f1o  40837  clsk1indlem1  41544