Definition df-2o 8435

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 8428	. 2 class 2o
2		c1o 8427	. . 3 class 1o
3	2	csuc 6334	. 2 class suc 1o
4	1, 3	wceq 1540	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8442  2on  8447  2on0  8448  ondif2  8466  o1p1e2  8504  o2p2e4  8505  oneo  8545  2onnALT  8607  1one2o  8610  nnm2  8617  nnneo  8619  nneob  8620  enpr2dOLD  9021  1sdom2ALT  9188  1sdomOLD  9196  en2  9226  pm54.43  9954  en2eleq  9961  en2other2  9962  infxpenc  9971  infxpenc2  9975  dju1p1e2ALT  10128  fin1a2lem4  10356  cfpwsdom  10537  canthp1lem2  10606  pwxpndom2  10618  tsk2  10718  hash2  14370  f1otrspeq  19377  pmtrf  19385  pmtrmvd  19386  pmtrfinv  19391  efgmnvl  19644  isnzr2  20427  sltval2  27568  nosgnn0  27570  sltsolem1  27587  nosepnelem  27591  nolt02o  27607  nogt01o  27608  unidifsnel  32464  unidifsnne  32465  ex-sategoelel12  35414  1oequni2o  37356  finxpreclem3  37381  finxpreclem4  37382  finxpsuclem  37385  finxp2o  37387  pw2f1ocnv  43026  pwfi2f1o  43085  oege2  43296  oaomoencom  43306  om2  43393  oaltom  43394  oe2  43395  omltoe  43396  nlim2NEW  43432  clsk1indlem1  44034