Definition df-2o 8475

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 8468	. 2 class 2o
2		c1o 8467	. . 3 class 1o
3	2	csuc 6351	. 2 class suc 1o
4	1, 3	wceq 1539	1 wff 2o = suc 1o

This definition is referenced by:  df2o3  8482  2on  8488  2onOLD  8489  2on0  8490  ondif2  8508  o1p1e2  8546  o2p2e4  8547  oneo  8587  2onnALT  8649  1one2o  8652  nnm2  8659  nnneo  8661  nneob  8662  enpr2dOLD  9058  snnen2oOLD  9230  1sdom2ALT  9243  1sdomOLD  9251  en2  9281  pm54.43  10007  en2eleq  10014  en2other2  10015  infxpenc  10024  infxpenc2  10028  dju1p1e2ALT  10181  fin1a2lem4  10409  cfpwsdom  10590  canthp1lem2  10659  pwxpndom2  10671  tsk2  10771  hash2  14411  f1otrspeq  19413  pmtrf  19421  pmtrmvd  19422  pmtrfinv  19427  efgmnvl  19680  isnzr2  20463  sltval2  27604  nosgnn0  27606  sltsolem1  27623  nosepnelem  27627  nolt02o  27643  nogt01o  27644  unidifsnel  32449  unidifsnne  32450  ex-sategoelel12  35370  1oequni2o  37307  finxpreclem3  37332  finxpreclem4  37333  finxpsuclem  37336  finxp2o  37338  pw2f1ocnv  42986  pwfi2f1o  43045  oege2  43256  oaomoencom  43266  om2  43353  oaltom  43354  oe2  43355  omltoe  43356  nlim2NEW  43392  clsk1indlem1  43994