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

Theorem df1o2 7149
Description: Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.)
Assertion
Ref Expression
df1o2  |-  1o  =  { (/) }

Proof of Theorem df1o2
StepHypRef Expression
1 df-1o 7137 . 2  |-  1o  =  suc  (/)
2 suc0 5459 . 2  |-  suc  (/)  =  { (/)
}
31, 2eqtri 2450 1  |-  1o  =  { (/) }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   (/)c0 3704   {csn 3941   suc csuc 5387   1oc1o 7130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-dif 3382  df-un 3384  df-nul 3705  df-suc 5391  df-1o 7137
This theorem is referenced by:  df2o3  7150  df2o2  7151  1n0  7152  el1o  7156  dif1o  7157  0we1  7163  oeeui  7258  ensn1  7587  en1  7590  map1  7602  xp1en  7611  map2xp  7695  pwfi  7822  infxpenlem  8396  fseqenlem1  8406  cda1dif  8557  infcda1  8574  pwcda1  8575  infmap2  8599  cflim2  8644  pwxpndom2  9041  pwcdandom  9043  gchxpidm  9045  wuncval2  9123  tsk1  9140  hashen1  12500  hashmap  12555  sylow2alem2  17213  psr1baslem  18721  fvcoe1  18743  coe1f2  18745  coe1sfi  18749  coe1add  18800  coe1mul2lem1  18803  coe1mul2lem2  18804  coe1mul2  18805  coe1tm  18809  ply1coe  18832  ply1coeOLD  18833  evls1rhmlem  18853  evl1sca  18865  evl1var  18867  pf1mpf  18883  pf1ind  18886  mat0dimbas0  19433  mavmul0g  19520  hmph0  20752  tdeglem2  22952  deg1ldg  22983  deg1leb  22986  deg1val  22987  bnj105  29482  bnj96  29628  bnj98  29630  bnj149  29638  rankeq1o  30887  ordcmp  31056  ssoninhaus  31057  onint1  31058  poimirlem28  31875  reheibor  32078  wopprc  35798  pwslnmlem0  35862  pwfi2f1o  35867  lincval0  39811  lco0  39823  linds0  39861
  Copyright terms: Public domain W3C validator