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 3694 | . 2 | |
2 | 1 | ibi 175 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wcel 2128 wss 3102 csn 3561 |
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 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-v 2714 df-in 3108 df-ss 3115 df-sn 3567 |
This theorem is referenced by: difsnss 3704 sssnm 3719 tpssi 3724 snelpwi 4174 intid 4186 abnexg 4408 ordsucss 4465 xpsspw 4700 djussxp 4733 xpimasn 5036 fconst6g 5370 f1sng 5458 fvimacnvi 5583 fsn2 5643 fnressn 5655 fsnunf 5669 mapsn 6637 unsnfidcel 6867 en1eqsn 6894 exmidfodomrlemim 7138 axresscn 7782 nn0ssre 9099 1fv 10047 fxnn0nninf 10346 1exp 10457 hashdifsn 10704 hashdifpr 10705 fsum00 11370 hash2iun1dif1 11388 exmidunben 12225 isneip 12616 neipsm 12624 opnneip 12629 |
Copyright terms: Public domain | W3C validator |