ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df1o2 GIF version

Theorem df1o2 6176
Description: Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.)
Assertion
Ref Expression
df1o2 1𝑜 = {∅}

Proof of Theorem df1o2
StepHypRef Expression
1 df-1o 6163 . 2 1𝑜 = suc ∅
2 suc0 4229 . 2 suc ∅ = {∅}
31, 2eqtri 2108 1 1𝑜 = {∅}
Colors of variables: wff set class
Syntax hints:   = wceq 1289  c0 3284  {csn 3441  suc csuc 4183  1𝑜c1o 6156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-dif 2999  df-un 3001  df-nul 3285  df-suc 4189  df-1o 6163
This theorem is referenced by:  df2o3  6177  df2o2  6178  1n0  6179  el1o  6183  dif1o  6184  ensn1  6493  en1  6496  map1  6509  xp1en  6519  exmidpw  6604  unfiexmid  6608  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  fihashen1  10172  ss1oel2o  11545  pw1dom2  11546
  Copyright terms: Public domain W3C validator