Theorem df1o2 8110

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 8096	. 2 ⊢ 1o = suc ∅
2		suc0 6260	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2844	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1533  ∅c0 4291  {csn 4561  suc csuc 6188  1_oc1o 8089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-dif 3939  df-un 3941  df-nul 4292  df-suc 6192  df-1o 8096

This theorem is referenced by:  df2o3  8111  df2o2  8112  1n0  8113  el1o  8118  dif1o  8119  0we1  8125  oeeui  8222  map0e  8440  ensn1  8567  en1  8570  map1  8586  xp1en  8597  pwfi  8813  infxpenlem  9433  fseqenlem1  9444  dju1dif  9592  infdju1  9609  pwdju1  9610  infmap2  9634  cflim2  9679  pwxpndom2  10081  pwdjundom  10083  gchxpidm  10085  wuncval2  10163  tsk1  10180  hashen1  13725  sylow2alem2  18737  psr1baslem  20347  fvcoe1  20369  coe1f2  20371  coe1sfi  20375  coe1add  20426  coe1mul2lem1  20429  coe1mul2lem2  20430  coe1mul2  20431  coe1tm  20435  ply1coe  20458  evls1rhmlem  20478  evl1sca  20491  evl1var  20493  pf1mpf  20509  pf1ind  20512  mat0dimbas0  21069  mavmul0g  21156  hmph0  22397  tdeglem2  24649  deg1ldg  24680  deg1leb  24683  deg1val  24684  fply1  30926  bnj105  31989  bnj96  32132  bnj98  32134  bnj149  32142  rankeq1o  33627  ordcmp  33790  ssoninhaus  33791  onint1  33792  poimirlem28  34914  reheibor  35111  wopprc  39620  pwslnmlem0  39684  pwfi2f1o  39689  lincval0  44463  lco0  44475  linds0  44513