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

Theorem df1o2 8103
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 8089 . 2 1o = suc ∅
2 suc0 6237 . 2 suc ∅ = {∅}
31, 2eqtri 2824 1 1o = {∅}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  c0 4246  {csn 4528  suc csuc 6165  1oc1o 8082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-dif 3887  df-un 3889  df-nul 4247  df-suc 6169  df-1o 8089
This theorem is referenced by:  df2o3  8104  df2o2  8105  1n0  8106  el1o  8111  dif1o  8112  0we1  8118  oeeui  8215  map0e  8433  ensn1  8560  en1  8563  map1  8579  xp1en  8590  pwfi  8807  infxpenlem  9428  fseqenlem1  9439  dju1dif  9587  infdju1  9604  pwdju1  9605  infmap2  9633  cflim2  9678  pwxpndom2  10080  pwdjundom  10082  gchxpidm  10084  wuncval2  10162  tsk1  10179  hashen1  13731  sylow2alem2  18738  psr1baslem  20817  fvcoe1  20839  coe1f2  20841  coe1sfi  20845  coe1add  20896  coe1mul2lem1  20899  coe1mul2lem2  20900  coe1mul2  20901  coe1tm  20905  ply1coe  20928  evls1rhmlem  20948  evl1sca  20961  evl1var  20963  pf1mpf  20979  pf1ind  20982  mat0dimbas0  21074  mavmul0g  21161  hmph0  22403  tdeglem2  24665  deg1ldg  24696  deg1leb  24699  deg1val  24700  fply1  30985  bnj105  32102  bnj96  32245  bnj98  32247  bnj149  32255  rankeq1o  33740  ordcmp  33903  ssoninhaus  33904  onint1  33905  poimirlem28  35078  reheibor  35270  wopprc  39958  pwslnmlem0  40022  pwfi2f1o  40027  lincval0  44811  lco0  44823  linds0  44861
  Copyright terms: Public domain W3C validator