| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > snssi | GIF 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 3767 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) | |
| 2 | 1 | ibi 176 | 1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∈ wcel 2176 ⊆ wss 3166 {csn 3633 |
| 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-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-v 2774 df-in 3172 df-ss 3179 df-sn 3639 |
| This theorem is referenced by: difsnss 3779 sssnm 3795 tpssi 3800 snelpwi 4256 intid 4268 abnexg 4493 ordsucss 4552 xpsspw 4787 djussxp 4823 xpimasn 5131 fconst6g 5474 f1sng 5564 fvimacnvi 5694 fsn2 5754 fnressn 5770 fsnunf 5784 mapsn 6777 unsnfidcel 7018 en1eqsn 7050 exmidfodomrlemim 7309 axresscn 7973 nn0ssre 9299 1fv 10261 fxnn0nninf 10584 1exp 10713 hashdifsn 10964 hashdifpr 10965 fsum00 11773 hash2iun1dif1 11791 4sqlem19 12732 exmidunben 12797 lspsncl 14154 lspsnss 14166 lspsnid 14169 znlidl 14396 isneip 14618 neipsm 14626 opnneip 14631 plyun0 15208 plycjlemc 15232 plycj 15233 plyrecj 15235 dvply2g 15238 perfectlem2 15472 |
| Copyright terms: Public domain | W3C validator |