| 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 4815 | . . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵} | |
| 2 | ssun1 4178 | . . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶}) | |
| 3 | 1, 2 | sstri 3993 | . 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶}) |
| 4 | df-tp 4631 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | |
| 5 | 3, 4 | sseqtrri 4033 | 1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶} |
| Colors of variables: wff setvar class |
| Syntax hints: ∪ cun 3949 ⊆ wss 3951 {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 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-ss 3968 df-pr 4629 df-tp 4631 |
| This theorem is referenced by: fr3nr 7792 rngplusg 17344 srngplusg 17355 lmodplusg 17371 ipsaddg 17382 ipsvsca 17385 phlplusg 17392 topgrpplusg 17407 otpstset 17422 odrngplusg 17449 odrngle 17452 prdsplusg 17503 prdsvsca 17505 prdsle 17507 imasplusg 17562 imasvsca 17565 imasle 17568 fuchom 18009 setchomfval 18124 catchomfval 18147 estrchomfval 18170 xpchomfval 18224 mpocnfldadd 21369 cnfldle 21375 cnfldaddOLD 21384 cnfldleOLD 21388 psrplusg 21956 psrvscafval 21968 trkgdist 28454 rlocaddval 33272 idlsrgplusg 33533 algaddg 43187 clsk1indlem4 44057 rngchomfvalALTV 48183 ringchomfvalALTV 48217 mndtchom 49181 |
| Copyright terms: Public domain | W3C validator |