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

Theorem df1o2 6930
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 6918 . 2  |-  1o  =  suc  (/)
2 suc0 4791 . 2  |-  suc  (/)  =  { (/)
}
31, 2eqtri 2461 1  |-  1o  =  { (/) }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369   (/)c0 3635   {csn 3875   suc csuc 4719   1oc1o 6911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-dif 3329  df-un 3331  df-nul 3636  df-suc 4723  df-1o 6918
This theorem is referenced by:  df2o3  6931  df2o2  6932  1n0  6933  el1o  6937  dif1o  6938  0we1  6944  oeeui  7039  ensn1  7371  en1  7374  map1  7386  xp1en  7395  map2xp  7479  pwfi  7604  cantnffvalOLD  7869  cantnfp1lem1OLD  7910  cantnfp1lem3OLD  7912  cantnflem1dOLD  7917  cantnflem1OLD  7918  wemapweOLD  7927  oef1oOLD  7929  cnfcom2lemOLD  7940  infxpenlem  8178  fseqenlem1  8192  cda1dif  8343  infcda1  8360  pwcda1  8361  infmap2  8385  cflim2  8430  pwxpndom2  8830  pwcdandom  8832  gchxpidm  8834  wuncval2  8912  tsk1  8929  hashmap  12195  sylow2alem2  16115  psr1baslem  17639  fvcoe1  17661  coe1f2  17663  coe1sfi  17666  coe1sfiOLD  17667  coe1add  17716  coe1mul2lem1  17719  coe1mul2lem2  17720  coe1mul2  17721  coe1tm  17724  ply1coe  17744  ply1coeOLD  17745  evls1rhmlem  17754  evl1sca  17766  evl1var  17768  pf1mpf  17784  pf1ind  17787  mat0dimbas0  18323  mavmul0g  18362  hmph0  19366  tdeglem2  21528  deg1ldg  21561  deg1leb  21564  deg1val  21565  deg1valOLD  21566  rankeq1o  28207  ordcmp  28291  ssoninhaus  28292  onint1  28293  reheibor  28735  wopprc  29376  pwslnmlem0  29441  pwfi2f1o  29448  hashen1  30734  lincval0  30946  lco0  30958  linds0  30996  bnj105  31710  bnj96  31855  bnj98  31857  bnj149  31865
  Copyright terms: Public domain W3C validator