Definition df-2o 7425

Description: Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.)

Assertion

Ref	Expression
df-2o	⊢ 2𝑜 = suc 1𝑜

Detailed syntax breakdown of Definition df-2o

Step	Hyp	Ref	Expression
1		c2o 7418	. 2 class 2𝑜
2		c1o 7417	. . 3 class 1𝑜
3	2	csuc 5627	. 2 class suc 1𝑜
4	1, 3	wceq 1474	1 wff 2𝑜 = suc 1𝑜

This definition is referenced by:  2on  7432  2on0  7433  df2o3  7437  ondif2  7446  o1p1e2  7484  o2p2e4  7485  oneo  7525  2onn  7584  nnm2  7593  nnneo  7595  nneob  7596  snnen2o  8011  1sdom2  8021  1sdom  8025  en2  8058  pm54.43  8686  en2eleq  8691  en2other2  8692  infxpenc  8701  infxpenc2  8705  pm110.643ALT  8860  fin1a2lem4  9085  cfpwsdom  9262  canthp1lem2  9331  pwxpndom2  9343  tsk2  9443  hash2  13008  f1otrspeq  17638  pmtrf  17646  pmtrmvd  17647  pmtrfinv  17652  efgmnvl  17898  isnzr2  19032  sltval2  30846  nosgnn0  30848  sltsolem1  30860  bj-2ex  31915  1oequni2o  32175  finxpreclem3  32189  finxpreclem4  32190  finxpsuclem  32193  finxp2o  32195  pw2f1ocnv  36405  pwfi2f1o  36467  clsk1indlem1  37146