Theorem df1o2 7459

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 7447	. 2 ⊢ 1𝑜 = suc ∅
2		suc0 5716	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2632	1 ⊢ 1𝑜 = {∅}

Syntax hints:   = wceq 1475  ∅c0 3874  {csn 4125  suc csuc 5642  1_𝑜c1o 7440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-un 3545  df-nul 3875  df-suc 5646  df-1o 7447

This theorem is referenced by:  df2o3  7460  df2o2  7461  1n0  7462  el1o  7466  dif1o  7467  0we1  7473  oeeui  7569  ensn1  7906  en1  7909  map1  7921  xp1en  7931  map2xp  8015  pwfi  8144  infxpenlem  8719  fseqenlem1  8730  cda1dif  8881  infcda1  8898  pwcda1  8899  infmap2  8923  cflim2  8968  pwxpndom2  9366  pwcdandom  9368  gchxpidm  9370  wuncval2  9448  tsk1  9465  hashen1  13021  hashmap  13082  sylow2alem2  17856  psr1baslem  19376  fvcoe1  19398  coe1f2  19400  coe1sfi  19404  coe1add  19455  coe1mul2lem1  19458  coe1mul2lem2  19459  coe1mul2  19460  coe1tm  19464  ply1coe  19487  evls1rhmlem  19507  evl1sca  19519  evl1var  19521  pf1mpf  19537  pf1ind  19540  mat0dimbas0  20091  mavmul0g  20178  hmph0  21408  tdeglem2  23625  deg1ldg  23656  deg1leb  23659  deg1val  23660  bnj105  30044  bnj96  30189  bnj98  30191  bnj149  30199  rankeq1o  31448  ordcmp  31616  ssoninhaus  31617  onint1  31618  poimirlem28  32607  reheibor  32808  wopprc  36615  pwslnmlem0  36679  pwfi2f1o  36684  lincval0  41998  lco0  42010  linds0  42048