![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > snsstp2 | Structured version Visualization version GIF version |
Description: A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.) |
Ref | Expression |
---|---|
snsstp2 | ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snsspr2 4817 | . . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵} | |
2 | ssun1 4171 | . . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶}) | |
3 | 1, 2 | sstri 3990 | . 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶}) |
4 | df-tp 4632 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | |
5 | 3, 4 | sseqtrri 4018 | 1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶} |
Colors of variables: wff setvar class |
Syntax hints: ∪ cun 3945 ⊆ wss 3947 {csn 4627 {cpr 4629 {ctp 4631 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-v 3474 df-un 3952 df-in 3954 df-ss 3964 df-pr 4630 df-tp 4632 |
This theorem is referenced by: fr3nr 7761 rngplusg 17249 srngplusg 17260 lmodplusg 17276 ipsaddg 17287 ipsvsca 17290 phlplusg 17297 topgrpplusg 17312 otpstset 17327 odrngplusg 17354 odrngle 17357 prdsplusg 17408 prdsvsca 17410 prdsle 17412 imasplusg 17467 imasvsca 17470 imasle 17473 fuchom 17917 fuchomOLD 17918 setchomfval 18033 catchomfval 18056 estrchomfval 18081 xpchomfval 18135 cnfldadd 21149 cnfldle 21153 psrplusg 21719 psrvscafval 21728 trkgdist 27964 idlsrgplusg 32893 mpocnfldadd 35476 gg-cnfldle 35480 algaddg 42223 clsk1indlem4 43097 rngchomfvalALTV 46970 ringchomfvalALTV 47033 mndtchom 47797 |
Copyright terms: Public domain | W3C validator |