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

Theorem df1o2 7518
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 7506 . 2 1𝑜 = suc ∅
2 suc0 5761 . 2 suc ∅ = {∅}
31, 2eqtri 2648 1 1𝑜 = {∅}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  c0 3896  {csn 4153  suc csuc 5687  1𝑜c1o 7499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-dif 3563  df-un 3565  df-nul 3897  df-suc 5691  df-1o 7506
This theorem is referenced by:  df2o3  7519  df2o2  7520  1n0  7521  el1o  7525  dif1o  7526  0we1  7532  oeeui  7628  ensn1  7965  en1  7968  map1  7981  xp1en  7991  map2xp  8075  pwfi  8206  infxpenlem  8781  fseqenlem1  8792  cda1dif  8943  infcda1  8960  pwcda1  8961  infmap2  8985  cflim2  9030  pwxpndom2  9432  pwcdandom  9434  gchxpidm  9436  wuncval2  9514  tsk1  9531  hashen1  13097  hashmap  13159  sylow2alem2  17949  psr1baslem  19469  fvcoe1  19491  coe1f2  19493  coe1sfi  19497  coe1add  19548  coe1mul2lem1  19551  coe1mul2lem2  19552  coe1mul2  19553  coe1tm  19557  ply1coe  19580  evls1rhmlem  19600  evl1sca  19612  evl1var  19614  pf1mpf  19630  pf1ind  19633  mat0dimbas0  20186  mavmul0g  20273  hmph0  21503  tdeglem2  23720  deg1ldg  23751  deg1leb  23754  deg1val  23755  bnj105  30490  bnj96  30635  bnj98  30637  bnj149  30645  rankeq1o  31912  ordcmp  32080  ssoninhaus  32081  onint1  32082  poimirlem28  33055  reheibor  33256  wopprc  37063  pwslnmlem0  37127  pwfi2f1o  37132  lincval0  41466  lco0  41478  linds0  41516
  Copyright terms: Public domain W3C validator