![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df1o2 | GIF version |
Description: Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.) |
Ref | Expression |
---|---|
df1o2 | ⊢ 1o = {∅} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-1o 6321 | . 2 ⊢ 1o = suc ∅ | |
2 | suc0 4341 | . 2 ⊢ suc ∅ = {∅} | |
3 | 1, 2 | eqtri 2161 | 1 ⊢ 1o = {∅} |
Colors of variables: wff set class |
Syntax hints: = wceq 1332 ∅c0 3368 {csn 3532 suc csuc 4295 1oc1o 6314 |
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 604 ax-in2 605 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-v 2691 df-dif 3078 df-un 3080 df-nul 3369 df-suc 4301 df-1o 6321 |
This theorem is referenced by: df2o3 6335 df2o2 6336 1n0 6337 el1o 6342 dif1o 6343 ensn1 6698 en1 6701 map1 6714 xp1en 6725 exmidpw 6810 unfiexmid 6814 0ct 7000 exmidonfinlem 7066 exmidfodomrlemr 7075 exmidfodomrlemrALT 7076 fihashen1 10577 ss1oel2o 13360 pw1dom2 13361 pwle2 13366 pwf1oexmid 13367 sbthom 13396 |
Copyright terms: Public domain | W3C validator |