Theorem df1o2 7777

Description: Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.)

Assertion

Ref	Expression
df1o2	⊢ 1𝑜 = {∅}

Proof of Theorem df1o2

Step	Hyp	Ref	Expression
1		df-1o 7764	. 2 ⊢ 1𝑜 = suc ∅
2		suc0 5982	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2787	1 ⊢ 1𝑜 = {∅}

Syntax hints:   = wceq 1652  ∅c0 4079  {csn 4334  suc csuc 5910  1_𝑜c1o 7757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-dif 3735  df-un 3737  df-nul 4080  df-suc 5914  df-1o 7764

This theorem is referenced by:  df2o3  7778  df2o2  7779  1n0  7780  el1o  7784  dif1o  7785  0we1  7791  oeeui  7887  map0e  8098  ensn1  8224  en1  8227  map1  8243  xp1en  8253  pwfi  8468  infxpenlem  9087  fseqenlem1  9098  cda1dif  9251  infcda1  9268  pwcda1  9269  infmap2  9293  cflim2  9338  pwxpndom2  9740  pwcdandom  9742  gchxpidm  9744  wuncval2  9822  tsk1  9839  hashen1  13362  sylow2alem2  18299  psr1baslem  19828  fvcoe1  19850  coe1f2  19852  coe1sfi  19856  coe1add  19907  coe1mul2lem1  19910  coe1mul2lem2  19911  coe1mul2  19912  coe1tm  19916  ply1coe  19939  evls1rhmlem  19959  evl1sca  19971  evl1var  19973  pf1mpf  19989  pf1ind  19992  mat0dimbas0  20549  mavmul0g  20636  hmph0  21878  tdeglem2  24112  deg1ldg  24143  deg1leb  24146  deg1val  24147  bnj105  31173  bnj96  31315  bnj98  31317  bnj149  31325  rankeq1o  32654  ordcmp  32817  ssoninhaus  32818  onint1  32819  poimirlem28  33793  reheibor  33992  wopprc  38206  pwslnmlem0  38270  pwfi2f1o  38275  lincval0  42805  lco0  42817  linds0  42855