![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > snsstp3 | 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 |
---|---|
snsstp3 | ⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssun2 4171 | . 2 ⊢ {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶}) | |
2 | df-tp 4635 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | |
3 | 1, 2 | sseqtrri 4014 | 1 ⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶} |
Colors of variables: wff setvar class |
Syntax hints: ∪ cun 3942 ⊆ wss 3944 {csn 4630 {cpr 4632 {ctp 4634 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-v 3463 df-un 3949 df-ss 3961 df-tp 4635 |
This theorem is referenced by: fr3nr 7775 rngmulr 17285 srngmulr 17296 lmodsca 17312 ipsmulr 17323 ipsip 17326 phlsca 17333 topgrptset 17348 otpsle 17363 odrngmulr 17390 odrngds 17393 prdsmulr 17444 prdsip 17446 prdsds 17449 imasds 17498 imasmulr 17503 imasip 17506 fuccofval 17953 setccofval 18074 catccofval 18096 estrccofval 18122 xpccofval 18176 mpocnfldmul 21303 cnfldds 21308 cnfldmulOLD 21317 cnflddsOLD 21321 psrmulr 21904 trkgitv 28323 rlocmulval 33059 idlsrgmulr 33319 signswch 34324 algmulr 42746 clsk1indlem1 43617 rngccofvalALTV 47518 ringccofvalALTV 47552 mndtcco 48283 |
Copyright terms: Public domain | W3C validator |