Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > snssi | Unicode version |
Description: The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.) |
Ref | Expression |
---|---|
snssi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snssg 3651 | . 2 | |
2 | 1 | ibi 175 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 1480 wss 3066 csn 3522 |
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-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-v 2683 df-in 3072 df-ss 3079 df-sn 3528 |
This theorem is referenced by: difsnss 3661 sssnm 3676 tpssi 3681 snelpwi 4129 intid 4141 abnexg 4362 ordsucss 4415 xpsspw 4646 djussxp 4679 xpimasn 4982 fconst6g 5316 f1sng 5402 fvimacnvi 5527 fsn2 5587 fnressn 5599 fsnunf 5613 mapsn 6577 unsnfidcel 6802 en1eqsn 6829 exmidfodomrlemim 7050 axresscn 7661 nn0ssre 8974 1fv 9909 fxnn0nninf 10204 1exp 10315 hashdifsn 10558 hashdifpr 10559 fsum00 11224 hash2iun1dif1 11242 exmidunben 11928 isneip 12304 neipsm 12312 opnneip 12317 |
Copyright terms: Public domain | W3C validator |