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

Theorem df1o2 6695
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 6683 . 2  |-  1o  =  suc  (/)
2 suc0 4615 . 2  |-  suc  (/)  =  { (/)
}
31, 2eqtri 2424 1  |-  1o  =  { (/) }
Colors of variables: wff set class
Syntax hints:    = wceq 1649   (/)c0 3588   {csn 3774   suc csuc 4543   1oc1o 6676
This theorem is referenced by:  df2o3  6696  df2o2  6697  1n0  6698  el1o  6702  dif1o  6703  0we1  6709  oeeui  6804  ensn1  7130  en1  7133  map1  7144  xp1en  7153  map2xp  7236  pwfi  7360  cantnfp1lem1  7590  cantnfp1lem3  7592  oemapso  7594  cantnflem1d  7600  cantnflem1  7601  wemapwe  7610  oef1o  7611  cnfcom2lem  7614  infxpenlem  7851  fseqenlem1  7861  cda1dif  8012  infcda1  8029  pwcda1  8030  infmap2  8054  cflim2  8099  pwxpndom2  8496  pwcdandom  8498  gchxpidm  8500  wuncval2  8578  tsk1  8595  hashmap  11653  sylow2alem2  15207  psr1baslem  16538  fvcoe1  16560  coe1f2  16562  coe1sfi  16565  coe1add  16612  coe1mul2lem1  16615  coe1mul2lem2  16616  coe1mul2  16617  coe1tm  16620  ply1coe  16639  hmph0  17780  evl1rhm  19902  evl1sca  19903  evl1var  19905  pf1mpf  19925  pf1ind  19928  tdeglem2  19937  deg1ldg  19968  deg1leb  19971  deg1val  19972  rankeq1o  26016  ordcmp  26101  ssoninhaus  26102  onint1  26103  reheibor  26438  wopprc  26991  pwslnmlem0  27061  pwfi2f1o  27128  bnj105  28795  bnj96  28942  bnj98  28944  bnj149  28952
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283  df-un 3285  df-nul 3589  df-suc 4547  df-1o 6683
  Copyright terms: Public domain W3C validator