Definition df-2o 8285

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 8278	. 2 class 2o
2		c1o 8277	. . 3 class 1o
3	2	csuc 6261	. 2 class suc 1o
4	1, 3	wceq 1539	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8292  2on  8298  2onOLD  8299  2on0  8300  2oexOLD  8304  ondif2  8319  o1p1e2  8357  o2p2e4  8358  o2p2e4OLD  8359  oneo  8399  2onnALT  8460  1one2o  8463  nnm2  8470  nnneo  8472  nneob  8473  enpr2d  8825  snnen2oOLD  8997  1sdom2  9008  1sdom  9012  en2  9040  pm54.43  9769  en2eleq  9774  en2other2  9775  infxpenc  9784  infxpenc2  9788  dju1p1e2ALT  9940  fin1a2lem4  10169  cfpwsdom  10350  canthp1lem2  10419  pwxpndom2  10431  tsk2  10531  hash2  14130  f1otrspeq  19065  pmtrf  19073  pmtrmvd  19074  pmtrfinv  19079  efgmnvl  19330  isnzr2  20544  unidifsnel  30891  unidifsnne  30892  ex-sategoelel12  33397  sltval2  33867  nosgnn0  33869  sltsolem1  33886  nosepnelem  33890  nolt02o  33906  nogt01o  33907  1oequni2o  35547  finxpreclem3  35572  finxpreclem4  35573  finxpsuclem  35576  finxp2o  35578  pw2f1ocnv  40867  pwfi2f1o  40929  clsk1indlem1  41636