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

Theorem df1o2 7741
Description: Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.)
Assertion
Ref Expression
df1o2 1𝑜 = {∅}

Proof of Theorem df1o2
StepHypRef Expression
1 df-1o 7729 . 2 1𝑜 = suc ∅
2 suc0 5960 . 2 suc ∅ = {∅}
31, 2eqtri 2782 1 1𝑜 = {∅}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  c0 4058  {csn 4321  suc csuc 5886  1𝑜c1o 7722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718  df-un 3720  df-nul 4059  df-suc 5890  df-1o 7729
This theorem is referenced by:  df2o3  7742  df2o2  7743  1n0  7744  el1o  7748  dif1o  7749  0we1  7755  oeeui  7851  ensn1  8185  en1  8188  map1  8201  xp1en  8211  map2xp  8295  pwfi  8426  infxpenlem  9026  fseqenlem1  9037  cda1dif  9190  infcda1  9207  pwcda1  9208  infmap2  9232  cflim2  9277  pwxpndom2  9679  pwcdandom  9681  gchxpidm  9683  wuncval2  9761  tsk1  9778  hashen1  13352  hashmap  13414  sylow2alem2  18233  psr1baslem  19757  fvcoe1  19779  coe1f2  19781  coe1sfi  19785  coe1add  19836  coe1mul2lem1  19839  coe1mul2lem2  19840  coe1mul2  19841  coe1tm  19845  ply1coe  19868  evls1rhmlem  19888  evl1sca  19900  evl1var  19902  pf1mpf  19918  pf1ind  19921  mat0dimbas0  20474  mavmul0g  20561  hmph0  21800  tdeglem2  24020  deg1ldg  24051  deg1leb  24054  deg1val  24055  bnj105  31099  bnj96  31242  bnj98  31244  bnj149  31252  rankeq1o  32584  ordcmp  32752  ssoninhaus  32753  onint1  32754  poimirlem28  33750  reheibor  33951  wopprc  38099  pwslnmlem0  38163  pwfi2f1o  38168  lincval0  42714  lco0  42726  linds0  42764
  Copyright terms: Public domain W3C validator