Theorem df1o2 6545

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 6532	. 2 ⊢ 1o = suc ∅
2		suc0 4479	. 2 ⊢ suc ∅ = {∅}
3	1, 2	eqtri 2230	1 ⊢ 1o = {∅}

Syntax hints:   = wceq 1375  ∅c0 3471  {csn 3646  suc csuc 4433  1_oc1o 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-v 2781  df-dif 3179  df-un 3181  df-nul 3472  df-suc 4439  df-1o 6532

This theorem is referenced by:  df2o3  6546  df2o2  6547  1n0  6548  el1o  6553  dif1o  6554  ensn1  6918  en1  6921  map1  6935  xp1en  6950  exmidpw  7038  exmidpweq  7039  pw1fin  7040  pw1dc0el  7041  exmidpw2en  7042  ss1o0el1o  7043  unfiexmid  7048  0ct  7242  exmidonfinlem  7339  exmidfodomrlemr  7348  exmidfodomrlemrALT  7349  pw1m  7377  pw1on  7379  pw1dom2  7380  pw1ne1  7382  sucpw1nel3  7386  fihashen1  10988  ss1oel2o  16265  dom1o  16266  pwle2  16275  pwf1oexmid  16276  sbthom  16305