Theorem df1o2 7572

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 7560	. 2 |- 1o = suc (/)
2		suc0 5799	. 2 |- suc (/) = { (/) }
3	1, 2	eqtri 2644	1 |- 1o = { (/) }

Syntax hints:   = wceq 1483   (/)c0 3915   {csn 4177   suc csuc 5725   1oc1o 7553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-nul 3916  df-suc 5729  df-1o 7560

This theorem is referenced by:  df2o3  7573  df2o2  7574  1n0  7575  el1o  7579  dif1o  7580  0we1  7586  oeeui  7682  ensn1  8020  en1  8023  map1  8036  xp1en  8046  map2xp  8130  pwfi  8261  infxpenlem  8836  fseqenlem1  8847  cda1dif  8998  infcda1  9015  pwcda1  9016  infmap2  9040  cflim2  9085  pwxpndom2  9487  pwcdandom  9489  gchxpidm  9491  wuncval2  9569  tsk1  9586  hashen1  13160  hashmap  13222  sylow2alem2  18033  psr1baslem  19555  fvcoe1  19577  coe1f2  19579  coe1sfi  19583  coe1add  19634  coe1mul2lem1  19637  coe1mul2lem2  19638  coe1mul2  19639  coe1tm  19643  ply1coe  19666  evls1rhmlem  19686  evl1sca  19698  evl1var  19700  pf1mpf  19716  pf1ind  19719  mat0dimbas0  20272  mavmul0g  20359  hmph0  21598  tdeglem2  23821  deg1ldg  23852  deg1leb  23855  deg1val  23856  bnj105  30790  bnj96  30935  bnj98  30937  bnj149  30945  rankeq1o  32278  ordcmp  32446  ssoninhaus  32447  onint1  32448  poimirlem28  33437  reheibor  33638  wopprc  37597  pwslnmlem0  37661  pwfi2f1o  37666  lincval0  42204  lco0  42216  linds0  42254