Theorem df1o2 7920

Description: Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.)

Assertion

Ref	Expression
df1o2	⊢ 1o = {∅}

Proof of Theorem df1o2

Step	Hyp	Ref	Expression
1		df-1o 7907	. 2 ⊢ 1o = suc ∅
2		suc0 6105	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2802	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1507  ∅c0 4180  {csn 4442  suc csuc 6033  1_oc1o 7900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-v 3417  df-dif 3834  df-un 3836  df-nul 4181  df-suc 6037  df-1o 7907

This theorem is referenced by:  df2o3  7921  df2o2  7922  1n0  7923  el1o  7928  dif1o  7929  0we1  7935  oeeui  8031  map0e  8247  ensn1  8372  en1  8375  map1  8391  xp1en  8401  pwfi  8616  infxpenlem  9235  fseqenlem1  9246  dju1dif  9398  infdju1  9415  pwdju1  9416  infmap2  9440  cflim2  9485  pwxpndom2  9887  pwdjundom  9889  gchxpidm  9891  wuncval2  9969  tsk1  9986  hashen1  13548  sylow2alem2  18507  psr1baslem  20059  fvcoe1  20081  coe1f2  20083  coe1sfi  20087  coe1add  20138  coe1mul2lem1  20141  coe1mul2lem2  20142  coe1mul2  20143  coe1tm  20147  ply1coe  20170  evls1rhmlem  20190  evl1sca  20202  evl1var  20204  pf1mpf  20220  pf1ind  20223  mat0dimbas0  20782  mavmul0g  20869  hmph0  22110  tdeglem2  24361  deg1ldg  24392  deg1leb  24395  deg1val  24396  fply1  30604  bnj105  31642  bnj96  31784  bnj98  31786  bnj149  31794  rankeq1o  33153  ordcmp  33315  ssoninhaus  33316  onint1  33317  poimirlem28  34361  reheibor  34559  wopprc  39023  pwslnmlem0  39087  pwfi2f1o  39092  lincval0  43838  lco0  43850  linds0  43888