Definition df-2o 7945

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 7938	. 2 class 2o
2		c1o 7937	. . 3 class 1o
3	2	csuc 6060	. 2 class suc 1o
4	1, 3	wceq 1520	1 wff 2o = suc 1o

This definition is referenced by:  2on  7953  2oex  7954  2on0  7955  df2o3  7959  ondif2  7969  o1p1e2  8007  o2p2e4  8008  oneo  8048  2onn  8107  1one2o  8110  nnm2  8117  nnneo  8119  nneob  8120  snnen2o  8543  1sdom2  8553  1sdom  8557  en2  8590  pm54.43  9264  en2eleq  9269  en2other2  9270  infxpenc  9279  infxpenc2  9283  dju1p1e2ALT  9435  fin1a2lem4  9660  cfpwsdom  9841  canthp1lem2  9910  pwxpndom2  9922  tsk2  10022  hash2  13602  f1otrspeq  18294  pmtrf  18302  pmtrmvd  18303  pmtrfinv  18308  efgmnvl  18555  isnzr2  19713  unidifsnel  29963  unidifsnne  29964  sltval2  32717  nosgnn0  32719  sltsolem1  32734  nosepnelem  32738  nolt02o  32753  1oequni2o  34126  finxpreclem3  34151  finxpreclem4  34152  finxpsuclem  34155  finxp2o  34157  pw2f1ocnv  39070  pwfi2f1o  39132  clsk1indlem1  39831  enpr2d  40003