Theorem df1o2 8279

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 8267	. 2 ⊢ 1o = suc ∅
2		suc0 6325	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2766	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1539  ∅c0 4253  {csn 4558  suc csuc 6253  1_oc1o 8260

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-suc 6257  df-1o 8267

This theorem is referenced by:  1oex  8280  df2o3  8282  df2o2  8283  1n0  8286  el1o  8291  dif1o  8292  0we1  8298  oeeui  8395  map0e  8628  ensn1  8761  ensn1OLD  8762  en1  8765  en1OLD  8766  map1  8784  xp1en  8798  pwfiOLD  9044  infxpenlem  9700  fseqenlem1  9711  dju1dif  9859  infdju1  9876  pwdju1  9877  infmap2  9905  cflim2  9950  pwxpndom2  10352  pwdjundom  10354  gchxpidm  10356  wuncval2  10434  tsk1  10451  hashen1  14013  sylow2alem2  19138  psr1baslem  21266  fvcoe1  21288  coe1f2  21290  coe1sfi  21294  coe1add  21345  coe1mul2lem1  21348  coe1mul2lem2  21349  coe1mul2  21350  coe1tm  21354  ply1coe  21377  evls1rhmlem  21397  evl1sca  21410  evl1var  21412  pf1mpf  21428  pf1ind  21431  mat0dimbas0  21523  mavmul0g  21610  hmph0  22854  tdeglem2  25131  deg1ldg  25162  deg1leb  25165  deg1val  25166  fply1  31569  bnj105  32603  bnj96  32745  bnj98  32747  bnj149  32755  ssttrcl  33701  ttrclss  33706  ttrclselem2  33712  rankeq1o  34400  ordcmp  34563  ssoninhaus  34564  onint1  34565  poimirlem28  35732  reheibor  35924  wopprc  40768  pwslnmlem0  40832  pwfi2f1o  40837  lincval0  45644  lco0  45656  linds0  45694