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

Theorem df1o2 7141
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 7129 . 2  |-  1o  =  suc  (/)
2 suc0 4939 . 2  |-  suc  (/)  =  { (/)
}
31, 2eqtri 2470 1  |-  1o  =  { (/) }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1381   (/)c0 3768   {csn 4011   suc csuc 4867   1oc1o 7122
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-dif 3462  df-un 3464  df-nul 3769  df-suc 4871  df-1o 7129
This theorem is referenced by:  df2o3  7142  df2o2  7143  1n0  7144  el1o  7148  dif1o  7149  0we1  7155  oeeui  7250  ensn1  7578  en1  7581  map1  7593  xp1en  7602  map2xp  7686  pwfi  7814  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  12415  hashmap  12469  sylow2alem2  16509  psr1baslem  18095  fvcoe1  18117  coe1f2  18119  coe1sfi  18123  coe1sfiOLD  18124  coe1add  18176  coe1mul2lem1  18179  coe1mul2lem2  18180  coe1mul2  18181  coe1tm  18185  ply1coe  18208  ply1coeOLD  18209  evls1rhmlem  18229  evl1sca  18241  evl1var  18243  pf1mpf  18259  pf1ind  18262  mat0dimbas0  18838  mavmul0g  18925  hmph0  20166  tdeglem2  22329  deg1ldg  22362  deg1leb  22365  deg1val  22366  deg1valOLD  22367  rankeq1o  29800  ordcmp  29884  ssoninhaus  29885  onint1  29886  reheibor  30307  wopprc  30944  pwslnmlem0  31009  pwfi2f1o  31016  lincval0  32746  lco0  32758  linds0  32796  bnj105  33505  bnj96  33651  bnj98  33653  bnj149  33661
  Copyright terms: Public domain W3C validator