Theorem df1o2 8192

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 8180	. 2 ⊢ 1o = suc ∅
2		suc0 6265	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2759	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1543  ∅c0 4223  {csn 4527  suc csuc 6193  1_oc1o 8173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-dif 3856  df-un 3858  df-nul 4224  df-suc 6197  df-1o 8180

This theorem is referenced by:  1oex  8193  df2o3  8195  df2o2  8196  1n0  8199  el1o  8204  dif1o  8205  0we1  8211  oeeui  8308  map0e  8541  ensn1  8672  ensn1OLD  8673  en1  8676  en1OLD  8677  map1  8695  xp1en  8709  pwfiOLD  8949  infxpenlem  9592  fseqenlem1  9603  dju1dif  9751  infdju1  9768  pwdju1  9769  infmap2  9797  cflim2  9842  pwxpndom2  10244  pwdjundom  10246  gchxpidm  10248  wuncval2  10326  tsk1  10343  hashen1  13902  sylow2alem2  18961  psr1baslem  21060  fvcoe1  21082  coe1f2  21084  coe1sfi  21088  coe1add  21139  coe1mul2lem1  21142  coe1mul2lem2  21143  coe1mul2  21144  coe1tm  21148  ply1coe  21171  evls1rhmlem  21191  evl1sca  21204  evl1var  21206  pf1mpf  21222  pf1ind  21225  mat0dimbas0  21317  mavmul0g  21404  hmph0  22646  tdeglem2  24913  deg1ldg  24944  deg1leb  24947  deg1val  24948  fply1  31335  bnj105  32369  bnj96  32512  bnj98  32514  bnj149  32522  rankeq1o  34159  ordcmp  34322  ssoninhaus  34323  onint1  34324  poimirlem28  35491  reheibor  35683  wopprc  40496  pwslnmlem0  40560  pwfi2f1o  40565  lincval0  45372  lco0  45384  linds0  45422