Definition df-2o 8103

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 8096	. 2 class 2o
2		c1o 8095	. . 3 class 1o
3	2	csuc 6193	. 2 class suc 1o
4	1, 3	wceq 1537	1 wff 2o = suc 1o

This definition is referenced by:  2on  8111  2oex  8112  2on0  8113  df2o3  8117  ondif2  8127  o1p1e2  8165  o2p2e4  8166  o2p2e4OLD  8167  oneo  8207  2onn  8266  1one2o  8269  nnm2  8276  nnneo  8278  nneob  8279  enpr2d  8597  snnen2o  8707  1sdom2  8717  1sdom  8721  en2  8754  pm54.43  9429  en2eleq  9434  en2other2  9435  infxpenc  9444  infxpenc2  9448  dju1p1e2ALT  9600  fin1a2lem4  9825  cfpwsdom  10006  canthp1lem2  10075  pwxpndom2  10087  tsk2  10187  hash2  13767  f1otrspeq  18575  pmtrf  18583  pmtrmvd  18584  pmtrfinv  18589  efgmnvl  18840  isnzr2  20036  unidifsnel  30295  unidifsnne  30296  ex-sategoelel12  32674  sltval2  33163  nosgnn0  33165  sltsolem1  33180  nosepnelem  33184  nolt02o  33199  1oequni2o  34652  finxpreclem3  34677  finxpreclem4  34678  finxpsuclem  34681  finxp2o  34683  pw2f1ocnv  39683  pwfi2f1o  39745  clsk1indlem1  40444