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

Theorem df1o2 7142
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 7130 . 2  |-  1o  =  suc  (/)
2 suc0 4952 . 2  |-  suc  (/)  =  { (/)
}
31, 2eqtri 2496 1  |-  1o  =  { (/) }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379   (/)c0 3785   {csn 4027   suc csuc 4880   1oc1o 7123
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479  df-un 3481  df-nul 3786  df-suc 4884  df-1o 7130
This theorem is referenced by:  df2o3  7143  df2o2  7144  1n0  7145  el1o  7149  dif1o  7150  0we1  7156  oeeui  7251  ensn1  7579  en1  7582  map1  7594  xp1en  7603  map2xp  7687  pwfi  7815  cantnffvalOLD  8082  cantnfp1lem1OLD  8123  cantnfp1lem3OLD  8125  cantnflem1dOLD  8130  cantnflem1OLD  8131  wemapweOLD  8140  oef1oOLD  8142  cnfcom2lemOLD  8153  infxpenlem  8391  fseqenlem1  8405  cda1dif  8556  infcda1  8573  pwcda1  8574  infmap2  8598  cflim2  8643  pwxpndom2  9043  pwcdandom  9045  gchxpidm  9047  wuncval2  9125  tsk1  9142  hashen1  12407  hashmap  12459  sylow2alem2  16444  psr1baslem  18023  fvcoe1  18045  coe1f2  18047  coe1sfi  18051  coe1sfiOLD  18052  coe1add  18104  coe1mul2lem1  18107  coe1mul2lem2  18108  coe1mul2  18109  coe1tm  18113  ply1coe  18136  ply1coeOLD  18137  evls1rhmlem  18157  evl1sca  18169  evl1var  18171  pf1mpf  18187  pf1ind  18190  mat0dimbas0  18763  mavmul0g  18850  hmph0  20059  tdeglem2  22222  deg1ldg  22255  deg1leb  22258  deg1val  22259  deg1valOLD  22260  rankeq1o  29433  ordcmp  29517  ssoninhaus  29518  onint1  29519  reheibor  29966  wopprc  30604  pwslnmlem0  30669  pwfi2f1o  30676  lincval0  32115  lco0  32127  linds0  32165  bnj105  32875  bnj96  33020  bnj98  33022  bnj149  33030
  Copyright terms: Public domain W3C validator