Definition df-2o 8505

Description: Define the ordinal number 2. Lemma 3.17 of [Schloeder] p. 10. (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 8498	. 2 class 2o
2		c1o 8497	. . 3 class 1o
3	2	csuc 6387	. 2 class suc 1o
4	1, 3	wceq 1536	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8512  2on  8518  2onOLD  8519  2on0  8520  ondif2  8538  o1p1e2  8576  o2p2e4  8577  oneo  8617  2onnALT  8679  1one2o  8682  nnm2  8689  nnneo  8691  nneob  8692  enpr2dOLD  9088  snnen2oOLD  9261  1sdom2ALT  9274  1sdomOLD  9282  en2  9312  pm54.43  10038  en2eleq  10045  en2other2  10046  infxpenc  10055  infxpenc2  10059  dju1p1e2ALT  10212  fin1a2lem4  10440  cfpwsdom  10621  canthp1lem2  10690  pwxpndom2  10702  tsk2  10802  hash2  14440  f1otrspeq  19479  pmtrf  19487  pmtrmvd  19488  pmtrfinv  19493  efgmnvl  19746  isnzr2  20534  sltval2  27715  nosgnn0  27717  sltsolem1  27734  nosepnelem  27738  nolt02o  27754  nogt01o  27755  unidifsnel  32560  unidifsnne  32561  ex-sategoelel12  35411  1oequni2o  37350  finxpreclem3  37375  finxpreclem4  37376  finxpsuclem  37379  finxp2o  37381  pw2f1ocnv  43025  pwfi2f1o  43084  oege2  43296  oaomoencom  43306  om2  43393  oaltom  43394  oe2  43395  omltoe  43396  nlim2NEW  43432  clsk1indlem1  44034