MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df1o2 Unicode version

Theorem df1o2 7161
Description: Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.)
Assertion
Ref Expression
df1o2

Proof of Theorem df1o2
StepHypRef Expression
1 df-1o 7149 . 2
2 suc0 4957 . 2
31, 2eqtri 2486 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395   c0 3784  {csn 4029  succsuc 4885   c1o 7142
This theorem is referenced by:  df2o3  7162  df2o2  7163  1n0  7164  el1o  7168  dif1o  7169  0we1  7175  oeeui  7270  ensn1  7599  en1  7602  map1  7614  xp1en  7623  map2xp  7707  pwfi  7835  cantnffvalOLD  8103  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  cantnflem1dOLD  8151  cantnflem1OLD  8152  wemapweOLD  8161  oef1oOLD  8163  cnfcom2lemOLD  8174  infxpenlem  8412  fseqenlem1  8426  cda1dif  8577  infcda1  8594  pwcda1  8595  infmap2  8619  cflim2  8664  pwxpndom2  9064  pwcdandom  9066  gchxpidm  9068  wuncval2  9146  tsk1  9163  hashen1  12439  hashmap  12493  sylow2alem2  16638  psr1baslem  18224  fvcoe1  18246  coe1f2  18248  coe1sfi  18252  coe1sfiOLD  18253  coe1add  18305  coe1mul2lem1  18308  coe1mul2lem2  18309  coe1mul2  18310  coe1tm  18314  ply1coe  18337  ply1coeOLD  18338  evls1rhmlem  18358  evl1sca  18370  evl1var  18372  pf1mpf  18388  pf1ind  18391  mat0dimbas0  18968  mavmul0g  19055  hmph0  20296  tdeglem2  22459  deg1ldg  22492  deg1leb  22495  deg1val  22496  deg1valOLD  22497  rankeq1o  29828  ordcmp  29912  ssoninhaus  29913  onint1  29914  reheibor  30335  wopprc  30972  pwslnmlem0  31037  pwfi2f1o  31044  lincval0  33016  lco0  33028  linds0  33066  bnj105  33777  bnj96  33923  bnj98  33925  bnj149  33933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-un 3480  df-nul 3785  df-suc 4889  df-1o 7149
  Copyright terms: Public domain W3C validator