Definition df-2o 8307

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 8300	. 2 class 2o
2		c1o 8299	. . 3 class 1o
3	2	csuc 6272	. 2 class suc 1o
4	1, 3	wceq 1539	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8314  2on  8320  2onOLD  8321  2on0  8322  2oexOLD  8326  ondif2  8341  o1p1e2  8379  o2p2e4  8380  o2p2e4OLD  8381  oneo  8421  2onnALT  8482  1one2o  8485  nnm2  8492  nnneo  8494  nneob  8495  enpr2d  8847  snnen2oOLD  9019  1sdom2  9030  1sdom  9034  en2  9062  pm54.43  9768  en2eleq  9773  en2other2  9774  infxpenc  9783  infxpenc2  9787  dju1p1e2ALT  9939  fin1a2lem4  10168  cfpwsdom  10349  canthp1lem2  10418  pwxpndom2  10430  tsk2  10530  hash2  14129  f1otrspeq  19064  pmtrf  19072  pmtrmvd  19073  pmtrfinv  19078  efgmnvl  19329  isnzr2  20543  unidifsnel  30892  unidifsnne  30893  ex-sategoelel12  33398  sltval2  33868  nosgnn0  33870  sltsolem1  33887  nosepnelem  33891  nolt02o  33907  nogt01o  33908  1oequni2o  35548  finxpreclem3  35573  finxpreclem4  35574  finxpsuclem  35577  finxp2o  35579  pw2f1ocnv  40866  pwfi2f1o  40928  nlim2NEW  41057  clsk1indlem1  41662