Theorem df1o2 8497

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 8490	. 2 ⊢ 1o = suc ∅
2		suc0 6447	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2786	1 ⊢ 1o = {∅}

This proof depends on syntax axioms:   = wceq 1569  ∅c0 4281  {csn 4588  suc csuc 6371  1_oc1o 8483

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050  df-un 4154  df-nul 4282  df-suc 6375  df-1o 8490

This theorem is used by:  df2o3  8498  df2o2  8499  1oex  8500  1n0OLD  8510  nlim1  8511  el1o  8517  dif1o  8522  0we1  8528  oeeui  8625  map0e  8924  ensn1  9062  en1  9065  map1  9082  xp1en  9096  0sdom1dom  9251  1sdom2  9253  sdom1  9255  1sdom2dom  9259  ssttrcl  9729  ttrclss  9734  ttrclselem2  9740  infxpenlem  10105  fseqenlem1  10116  dju1dif  10264  infdju1  10281  pwdju1  10282  infmap2  10308  pwxpndom2  10763  pwdjundom  10765  gchxpidm  10767  wuncval2  10845  tsk1  10862  hashen1  14527  sylow2alem2  19847  psr1baslem  22518  fvcoe1  22540  coe1f2  22542  coe1sfi  22546  coe1add  22598  coe1mul2lem1  22601  coe1mul2lem2  22602  coe1mul2  22603  coe1tm  22607  ply1coe  22631  evls1rhmlem  22654  evl1sca  22667  evl1var  22669  pf1mpf  22685  pf1ind  22688  mat0dimbas0  22796  mavmul0g  22883  hmph0  24129  tdeglem2  26394  deg1ldg  26425  deg1leb  26428  deg1val  26429  old1  28266  fply1  34146  selvply1rhmlema  34206  selvply1rhmlemb  34207  selvply1rhmlem1  34208  selvply1rhm0  34214  bnj105  35411  bnj96  35551  bnj98  35553  bnj149  35561  r11  35789  r12  35790  fineqvnttrclselem1  35863  rankeq1o  37062  nmulrid  37076  ordcmp  37365  ssoninhaus  37366  onint1  37367  poimirlem28  38709  reheibor  38916  wopprc  44180  pwslnmlem0  44236  pwfi2f1o  44241  nadd1suc  44537  lincval0  49669  lco0  49681  linds0  49719  f1omo  50149  setc1oterm  50768  setc1ohomfval  50770  setc1ocofval  50771  funcsetc1o  50774  isinito2lem  50775  setc1onsubc  50882