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

Theorem df1o2 7726
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 7713 . 2 1𝑜 = suc ∅
2 suc0 5942 . 2 suc ∅ = {∅}
31, 2eqtri 2793 1 1𝑜 = {∅}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  c0 4063  {csn 4316  suc csuc 5868  1𝑜c1o 7706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3726  df-un 3728  df-nul 4064  df-suc 5872  df-1o 7713
This theorem is referenced by:  df2o3  7727  df2o2  7728  1n0  7729  el1o  7733  dif1o  7734  0we1  7740  oeeui  7836  map0e  8047  ensn1  8173  en1  8176  map1  8192  xp1en  8202  pwfi  8417  infxpenlem  9036  fseqenlem1  9047  cda1dif  9200  infcda1  9217  pwcda1  9218  infmap2  9242  cflim2  9287  pwxpndom2  9689  pwcdandom  9691  gchxpidm  9693  wuncval2  9771  tsk1  9788  hashen1  13362  sylow2alem2  18240  psr1baslem  19770  fvcoe1  19792  coe1f2  19794  coe1sfi  19798  coe1add  19849  coe1mul2lem1  19852  coe1mul2lem2  19853  coe1mul2  19854  coe1tm  19858  ply1coe  19881  evls1rhmlem  19901  evl1sca  19913  evl1var  19915  pf1mpf  19931  pf1ind  19934  mat0dimbas0  20490  mavmul0g  20577  hmph0  21819  tdeglem2  24041  deg1ldg  24072  deg1leb  24075  deg1val  24076  bnj105  31130  bnj96  31273  bnj98  31275  bnj149  31283  rankeq1o  32615  ordcmp  32783  ssoninhaus  32784  onint1  32785  poimirlem28  33770  reheibor  33970  wopprc  38123  pwslnmlem0  38187  pwfi2f1o  38192  lincval0  42732  lco0  42744  linds0  42782
  Copyright terms: Public domain W3C validator