Theorem df1o2 8406

Description: Expanded value of the ordinal number 1. Definition 2.1 of [Schloeder] p. 4. (Contributed by NM, 4-Nov-2002.)

Assertion

Ref	Expression
df1o2	⊢ 1o = {∅}

Proof of Theorem df1o2

Step	Hyp	Ref	Expression
1		df-1o 8399	. 2 ⊢ 1o = suc ∅
2		suc0 6395	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2760	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1542  ∅c0 4274  {csn 4568  suc csuc 6320  1_oc1o 8392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-un 3895  df-nul 4275  df-suc 6324  df-1o 8399

This theorem is referenced by:  df2o3  8407  df2o2  8408  1oex  8409  1n0  8417  nlim1  8418  el1o  8424  dif1o  8429  0we1  8435  oeeui  8532  map0e  8824  ensn1  8962  en1  8965  map1  8981  xp1en  8995  0sdom1dom  9150  1sdom2  9152  sdom1  9154  1sdom2dom  9158  ssttrcl  9630  ttrclss  9635  ttrclselem2  9641  infxpenlem  9929  fseqenlem1  9940  dju1dif  10089  infdju1  10106  pwdju1  10107  infmap2  10133  cflim2  10179  pwxpndom2  10582  pwdjundom  10584  gchxpidm  10586  wuncval2  10664  tsk1  10681  hashen1  14326  sylow2alem2  19587  psr1baslem  22161  fvcoe1  22184  coe1f2  22186  coe1sfi  22190  coe1add  22242  coe1mul2lem1  22245  coe1mul2lem2  22246  coe1mul2  22247  coe1tm  22251  ply1coe  22276  evls1rhmlem  22299  evl1sca  22312  evl1var  22314  pf1mpf  22330  pf1ind  22333  mat0dimbas0  22444  mavmul0g  22531  hmph0  23773  tdeglem2  26039  deg1ldg  26070  deg1leb  26073  deg1val  26074  old1  27874  fply1  33636  bnj105  34886  bnj96  35026  bnj98  35028  bnj149  35036  r11  35256  r12  35257  fineqvnttrclselem1  35284  rankeq1o  36372  ordcmp  36648  ssoninhaus  36649  onint1  36650  poimirlem28  37986  reheibor  38177  wopprc  43479  pwslnmlem0  43540  pwfi2f1o  43545  nadd1suc  43841  lincval0  48906  lco0  48918  linds0  48956  f1omo  49383  setc1oterm  49981  setc1ohomfval  49983  setc1ocofval  49984  funcsetc1o  49987  isinito2lem  49988  setc1onsubc  50092