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

Theorem df1o2 8107
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 8093 . 2 1o = suc ∅
2 suc0 6259 . 2 suc ∅ = {∅}
31, 2eqtri 2844 1 1o = {∅}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  c0 4290  {csn 4559  suc csuc 6187  1oc1o 8086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-dif 3938  df-un 3940  df-nul 4291  df-suc 6191  df-1o 8093
This theorem is referenced by:  df2o3  8108  df2o2  8109  1n0  8110  el1o  8115  dif1o  8116  0we1  8122  oeeui  8218  map0e  8436  ensn1  8562  en1  8565  map1  8581  xp1en  8592  pwfi  8808  infxpenlem  9428  fseqenlem1  9439  dju1dif  9587  infdju1  9604  pwdju1  9605  infmap2  9629  cflim2  9674  pwxpndom2  10076  pwdjundom  10078  gchxpidm  10080  wuncval2  10158  tsk1  10175  hashen1  13721  sylow2alem2  18674  psr1baslem  20283  fvcoe1  20305  coe1f2  20307  coe1sfi  20311  coe1add  20362  coe1mul2lem1  20365  coe1mul2lem2  20366  coe1mul2  20367  coe1tm  20371  ply1coe  20394  evls1rhmlem  20414  evl1sca  20427  evl1var  20429  pf1mpf  20445  pf1ind  20448  mat0dimbas0  21005  mavmul0g  21092  hmph0  22333  tdeglem2  24584  deg1ldg  24615  deg1leb  24618  deg1val  24619  fply1  30859  bnj105  31894  bnj96  32037  bnj98  32039  bnj149  32047  rankeq1o  33530  ordcmp  33693  ssoninhaus  33694  onint1  33695  poimirlem28  34802  reheibor  35000  wopprc  39507  pwslnmlem0  39571  pwfi2f1o  39576  lincval0  44368  lco0  44380  linds0  44418
  Copyright terms: Public domain W3C validator