Theorem df1o2 8304

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

Syntax hints:   = wceq 1539  ∅c0 4256  {csn 4561  suc csuc 6268  1_oc1o 8290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-suc 6272  df-1o 8297

This theorem is referenced by:  df2o3  8305  df2o2  8306  1oex  8307  1n0  8318  nlim1  8319  el1o  8325  dif1o  8330  0we1  8336  oeeui  8433  map0e  8670  ensn1  8807  ensn1OLD  8808  en1  8811  en1OLD  8812  map1  8830  xp1en  8844  pwfiOLD  9114  ssttrcl  9473  ttrclss  9478  ttrclselem2  9484  infxpenlem  9769  fseqenlem1  9780  dju1dif  9928  infdju1  9945  pwdju1  9946  infmap2  9974  cflim2  10019  pwxpndom2  10421  pwdjundom  10423  gchxpidm  10425  wuncval2  10503  tsk1  10520  hashen1  14085  sylow2alem2  19223  psr1baslem  21356  fvcoe1  21378  coe1f2  21380  coe1sfi  21384  coe1add  21435  coe1mul2lem1  21438  coe1mul2lem2  21439  coe1mul2  21440  coe1tm  21444  ply1coe  21467  evls1rhmlem  21487  evl1sca  21500  evl1var  21502  pf1mpf  21518  pf1ind  21521  mat0dimbas0  21615  mavmul0g  21702  hmph0  22946  tdeglem2  25226  deg1ldg  25257  deg1leb  25260  deg1val  25261  fply1  31667  bnj105  32703  bnj96  32845  bnj98  32847  bnj149  32855  rankeq1o  34473  ordcmp  34636  ssoninhaus  34637  onint1  34638  poimirlem28  35805  reheibor  35997  wopprc  40852  pwslnmlem0  40916  pwfi2f1o  40921  lincval0  45756  lco0  45768  linds0  45806