![]() |
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 4816 | . . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵} | |
2 | ssun1 4170 | . . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶}) | |
3 | 1, 2 | sstri 3989 | . 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶}) |
4 | df-tp 4631 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | |
5 | 3, 4 | sseqtrri 4017 | 1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶} |
Colors of variables: wff setvar class |
Syntax hints: ∪ cun 3944 ⊆ wss 3946 {csn 4626 {cpr 4628 {ctp 4630 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3951 df-in 3953 df-ss 3963 df-pr 4629 df-tp 4631 |
This theorem is referenced by: fr3nr 7753 rngplusg 17240 srngplusg 17251 lmodplusg 17267 ipsaddg 17278 ipsvsca 17281 phlplusg 17288 topgrpplusg 17303 otpstset 17318 odrngplusg 17345 odrngle 17348 prdsplusg 17399 prdsvsca 17401 prdsle 17403 imasplusg 17458 imasvsca 17461 imasle 17464 fuchom 17908 fuchomOLD 17909 setchomfval 18024 catchomfval 18047 estrchomfval 18072 xpchomfval 18126 cnfldadd 20933 cnfldle 20937 psrplusg 21481 psrvscafval 21490 trkgdist 27676 idlsrgplusg 32570 algaddg 41853 clsk1indlem4 42727 rngchomfvalALTV 46783 ringchomfvalALTV 46846 mndtchom 47611 |
Copyright terms: Public domain | W3C validator |