Definition df-2o 7606

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 7599	. 2 class 2𝑜
2		c1o 7598	. . 3 class 1𝑜
3	2	csuc 5763	. 2 class suc 1𝑜
4	1, 3	wceq 1523	1 wff 2𝑜 = suc 1𝑜

This definition is referenced by:  2on  7613  2on0  7614  df2o3  7618  ondif2  7627  o1p1e2  7665  o2p2e4  7666  oneo  7706  2onn  7765  nnm2  7774  nnneo  7776  nneob  7777  snnen2o  8190  1sdom2  8200  1sdom  8204  en2  8237  pm54.43  8864  en2eleq  8869  en2other2  8870  infxpenc  8879  infxpenc2  8883  pm110.643ALT  9038  fin1a2lem4  9263  cfpwsdom  9444  canthp1lem2  9513  pwxpndom2  9525  tsk2  9625  hash2  13231  f1otrspeq  17913  pmtrf  17921  pmtrmvd  17922  pmtrfinv  17927  efgmnvl  18173  isnzr2  19311  sltval2  31934  nosgnn0  31936  sltsolem1  31951  nosepnelem  31955  nolt02o  31970  bj-2ex  33064  1oequni2o  33346  finxpreclem3  33360  finxpreclem4  33361  finxpsuclem  33364  finxp2o  33366  pw2f1ocnv  37921  pwfi2f1o  37983  clsk1indlem1  38660