Theorem df1o2 8118

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 8104	. 2 ⊢ 1o = suc ∅
2		suc0 6267	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2846	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1537  ∅c0 4293  {csn 4569  suc csuc 6195  1_oc1o 8097

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-dif 3941  df-un 3943  df-nul 4294  df-suc 6199  df-1o 8104

This theorem is referenced by:  df2o3  8119  df2o2  8120  1n0  8121  el1o  8126  dif1o  8127  0we1  8133  oeeui  8230  map0e  8448  ensn1  8575  en1  8578  map1  8594  xp1en  8605  pwfi  8821  infxpenlem  9441  fseqenlem1  9452  dju1dif  9600  infdju1  9617  pwdju1  9618  infmap2  9642  cflim2  9687  pwxpndom2  10089  pwdjundom  10091  gchxpidm  10093  wuncval2  10171  tsk1  10188  hashen1  13734  sylow2alem2  18745  psr1baslem  20355  fvcoe1  20377  coe1f2  20379  coe1sfi  20383  coe1add  20434  coe1mul2lem1  20437  coe1mul2lem2  20438  coe1mul2  20439  coe1tm  20443  ply1coe  20466  evls1rhmlem  20486  evl1sca  20499  evl1var  20501  pf1mpf  20517  pf1ind  20520  mat0dimbas0  21077  mavmul0g  21164  hmph0  22405  tdeglem2  24657  deg1ldg  24688  deg1leb  24691  deg1val  24692  fply1  30933  bnj105  31996  bnj96  32139  bnj98  32141  bnj149  32149  rankeq1o  33634  ordcmp  33797  ssoninhaus  33798  onint1  33799  poimirlem28  34922  reheibor  35119  wopprc  39634  pwslnmlem0  39698  pwfi2f1o  39703  lincval0  44477  lco0  44489  linds0  44527