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

Theorem df1o2 6728
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 6716 . 2  |-  1o  =  suc  (/)
2 suc0 4647 . 2  |-  suc  (/)  =  { (/)
}
31, 2eqtri 2455 1  |-  1o  =  { (/) }
Colors of variables: wff set class
Syntax hints:    = wceq 1652   (/)c0 3620   {csn 3806   suc csuc 4575   1oc1o 6709
This theorem is referenced by:  df2o3  6729  df2o2  6730  1n0  6731  el1o  6735  dif1o  6736  0we1  6742  oeeui  6837  ensn1  7163  en1  7166  map1  7177  xp1en  7186  map2xp  7269  pwfi  7394  cantnfp1lem1  7624  cantnfp1lem3  7626  oemapso  7628  cantnflem1d  7634  cantnflem1  7635  wemapwe  7644  oef1o  7645  cnfcom2lem  7648  infxpenlem  7885  fseqenlem1  7895  cda1dif  8046  infcda1  8063  pwcda1  8064  infmap2  8088  cflim2  8133  pwxpndom2  8530  pwcdandom  8532  gchxpidm  8534  wuncval2  8612  tsk1  8629  hashmap  11688  sylow2alem2  15242  psr1baslem  16573  fvcoe1  16595  coe1f2  16597  coe1sfi  16600  coe1add  16647  coe1mul2lem1  16650  coe1mul2lem2  16651  coe1mul2  16652  coe1tm  16655  ply1coe  16674  hmph0  17817  evl1rhm  19939  evl1sca  19940  evl1var  19942  pf1mpf  19962  pf1ind  19965  tdeglem2  19974  deg1ldg  20005  deg1leb  20008  deg1val  20009  rankeq1o  26077  ordcmp  26162  ssoninhaus  26163  onint1  26164  reheibor  26502  wopprc  27055  pwslnmlem0  27125  pwfi2f1o  27192  bnj105  28990  bnj96  29137  bnj98  29139  bnj149  29147
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-dif 3315  df-un 3317  df-nul 3621  df-suc 4579  df-1o 6716
  Copyright terms: Public domain W3C validator