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

Theorem df1o2 6507
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 6495 . 2  |-  1o  =  suc  (/)
2 suc0 4482 . 2  |-  suc  (/)  =  { (/)
}
31, 2eqtri 2316 1  |-  1o  =  { (/) }
Colors of variables: wff set class
Syntax hints:    = wceq 1632   (/)c0 3468   {csn 3653   suc csuc 4410   1oc1o 6488
This theorem is referenced by:  df2o3  6508  df2o2  6509  1n0  6510  el1o  6514  dif1o  6515  0we1  6521  oeeui  6616  ensn1  6941  en1  6944  map1  6955  xp1en  6964  map2xp  7047  pwfi  7167  cantnfp1lem1  7396  cantnfp1lem3  7398  oemapso  7400  cantnflem1d  7406  cantnflem1  7407  wemapwe  7416  oef1o  7417  cnfcom2lem  7420  infxpenlem  7657  fseqenlem1  7667  cda1dif  7818  infcda1  7835  pwcda1  7836  infmap2  7860  cflim2  7905  pwxpndom2  8303  pwcdandom  8305  gchxpidm  8307  wuncval2  8385  tsk1  8402  hashmap  11403  sylow2alem2  14945  psr1baslem  16280  fvcoe1  16304  coe1f2  16306  coe1sfi  16309  coe1add  16357  coe1mul2lem1  16360  coe1mul2lem2  16361  coe1mul2  16362  coe1tm  16365  ply1coe  16384  hmph0  17502  evl1rhm  19428  evl1sca  19429  evl1var  19431  pf1mpf  19451  pf1ind  19454  tdeglem2  19463  deg1ldg  19494  deg1leb  19497  deg1val  19498  rankeq1o  24873  ordcmp  24958  ssoninhaus  24959  onint1  24960  reheibor  26666  wopprc  27226  pwslnmlem0  27296  pwfi2f1o  27363  bnj105  29066  bnj96  29213  bnj98  29215  bnj149  29223
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-un 3170  df-nul 3469  df-suc 4414  df-1o 6495
  Copyright terms: Public domain W3C validator