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

Theorem df1o2 6491
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 6479 . 2  |-  1o  =  suc  (/)
2 suc0 4466 . 2  |-  suc  (/)  =  { (/)
}
31, 2eqtri 2303 1  |-  1o  =  { (/) }
Colors of variables: wff set class
Syntax hints:    = wceq 1623   (/)c0 3455   {csn 3640   suc csuc 4394   1oc1o 6472
This theorem is referenced by:  df2o3  6492  df2o2  6493  1n0  6494  el1o  6498  dif1o  6499  0we1  6505  oeeui  6600  ensn1  6925  en1  6928  map1  6939  xp1en  6948  map2xp  7031  pwfi  7151  cantnfp1lem1  7380  cantnfp1lem3  7382  oemapso  7384  cantnflem1d  7390  cantnflem1  7391  wemapwe  7400  oef1o  7401  cnfcom2lem  7404  infxpenlem  7641  fseqenlem1  7651  cda1dif  7802  infcda1  7819  pwcda1  7820  infmap2  7844  cflim2  7889  pwxpndom2  8287  pwcdandom  8289  gchxpidm  8291  wuncval2  8369  tsk1  8386  hashmap  11387  sylow2alem2  14929  psr1baslem  16264  fvcoe1  16288  coe1f2  16290  coe1sfi  16293  coe1add  16341  coe1mul2lem1  16344  coe1mul2lem2  16345  coe1mul2  16346  coe1tm  16349  ply1coe  16368  hmph0  17486  evl1rhm  19412  evl1sca  19413  evl1var  19415  pf1mpf  19435  pf1ind  19438  tdeglem2  19447  deg1ldg  19478  deg1leb  19481  deg1val  19482  rankeq1o  24801  ordcmp  24886  ssoninhaus  24887  onint1  24888  reheibor  26563  wopprc  27123  pwslnmlem0  27193  pwfi2f1o  27260  bnj105  28750  bnj96  28897  bnj98  28899  bnj149  28907
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-un 3157  df-nul 3456  df-suc 4398  df-1o 6479
  Copyright terms: Public domain W3C validator