Theorem df1o2 6408

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 6395	. 2 ⊢ 1o = suc ∅
2		suc0 4396	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2191	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1348  ∅c0 3414  {csn 3583  suc csuc 4350  1_oc1o 6388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-dif 3123  df-un 3125  df-nul 3415  df-suc 4356  df-1o 6395

This theorem is referenced by:  df2o3  6409  df2o2  6410  1n0  6411  el1o  6416  dif1o  6417  ensn1  6774  en1  6777  map1  6790  xp1en  6801  exmidpw  6886  exmidpweq  6887  pw1fin  6888  pw1dc0el  6889  ss1o0el1o  6890  unfiexmid  6895  0ct  7084  exmidonfinlem  7170  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  pw1on  7203  pw1dom2  7204  pw1ne1  7206  sucpw1nel3  7210  fihashen1  10734  ss1oel2o  14026  pwle2  14031  pwf1oexmid  14032  sbthom  14058