Theorem df1o2 8352

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 8345	. 2 ⊢ 1o = suc ∅
2		suc0 6362	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2764	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1540  ∅c0 4266  {csn 4570  suc csuc 6290  1_oc1o 8338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3442  df-dif 3899  df-un 3901  df-nul 4267  df-suc 6294  df-1o 8345

This theorem is referenced by:  df2o3  8353  df2o2  8354  1oex  8355  1n0  8367  nlim1  8368  el1o  8374  dif1o  8379  0we1  8385  oeeui  8482  map0e  8719  ensn1  8860  ensn1OLD  8861  en1  8864  en1OLD  8865  map1  8883  xp1en  8900  0sdom1dom  9081  1sdom2  9083  sdom1  9085  1sdom2dom  9090  pwfiOLD  9190  ssttrcl  9550  ttrclss  9555  ttrclselem2  9561  infxpenlem  9848  fseqenlem1  9859  dju1dif  10007  infdju1  10024  pwdju1  10025  infmap2  10053  cflim2  10098  pwxpndom2  10500  pwdjundom  10502  gchxpidm  10504  wuncval2  10582  tsk1  10599  hashen1  14163  sylow2alem2  19296  psr1baslem  21436  fvcoe1  21458  coe1f2  21460  coe1sfi  21464  coe1add  21515  coe1mul2lem1  21518  coe1mul2lem2  21519  coe1mul2  21520  coe1tm  21524  ply1coe  21547  evls1rhmlem  21567  evl1sca  21580  evl1var  21582  pf1mpf  21598  pf1ind  21601  mat0dimbas0  21695  mavmul0g  21782  hmph0  23026  tdeglem2  25306  deg1ldg  25337  deg1leb  25340  deg1val  25341  fply1  31802  bnj105  32839  bnj96  32980  bnj98  32982  bnj149  32990  rankeq1o  34543  ordcmp  34706  ssoninhaus  34707  onint1  34708  poimirlem28  35882  reheibor  36074  wopprc  41074  pwslnmlem0  41138  pwfi2f1o  41143  lincval0  46026  lco0  46038  linds0  46076