Theorem df1o2 7726

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 7713	. 2 ⊢ 1𝑜 = suc ∅
2		suc0 5942	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2793	1 ⊢ 1𝑜 = {∅}

Syntax hints:   = wceq 1631  ∅c0 4063  {csn 4316  suc csuc 5868  1_𝑜c1o 7706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3726  df-un 3728  df-nul 4064  df-suc 5872  df-1o 7713

This theorem is referenced by:  df2o3  7727  df2o2  7728  1n0  7729  el1o  7733  dif1o  7734  0we1  7740  oeeui  7836  map0e  8047  ensn1  8173  en1  8176  map1  8192  xp1en  8202  pwfi  8417  infxpenlem  9036  fseqenlem1  9047  cda1dif  9200  infcda1  9217  pwcda1  9218  infmap2  9242  cflim2  9287  pwxpndom2  9689  pwcdandom  9691  gchxpidm  9693  wuncval2  9771  tsk1  9788  hashen1  13362  sylow2alem2  18240  psr1baslem  19770  fvcoe1  19792  coe1f2  19794  coe1sfi  19798  coe1add  19849  coe1mul2lem1  19852  coe1mul2lem2  19853  coe1mul2  19854  coe1tm  19858  ply1coe  19881  evls1rhmlem  19901  evl1sca  19913  evl1var  19915  pf1mpf  19931  pf1ind  19934  mat0dimbas0  20490  mavmul0g  20577  hmph0  21819  tdeglem2  24041  deg1ldg  24072  deg1leb  24075  deg1val  24076  bnj105  31130  bnj96  31273  bnj98  31275  bnj149  31283  rankeq1o  32615  ordcmp  32783  ssoninhaus  32784  onint1  32785  poimirlem28  33770  reheibor  33970  wopprc  38123  pwslnmlem0  38187  pwfi2f1o  38192  lincval0  42732  lco0  42744  linds0  42782