![]() |
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 3928 | . 2 ⊢ {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶}) | |
2 | df-tp 4322 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | |
3 | 1, 2 | sseqtr4i 3787 | 1 ⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶} |
Colors of variables: wff setvar class |
Syntax hints: ∪ cun 3721 ⊆ wss 3723 {csn 4317 {cpr 4319 {ctp 4321 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-v 3353 df-un 3728 df-in 3730 df-ss 3737 df-tp 4322 |
This theorem is referenced by: fr3nr 7130 rngmulr 16211 srngmulr 16219 lmodsca 16228 ipsmulr 16235 ipsip 16238 phlsca 16245 topgrptset 16253 otpsle 16262 otpsleOLD 16266 odrngmulr 16277 odrngds 16280 prdsmulr 16327 prdsip 16329 prdsds 16332 imasds 16381 imasmulr 16386 imasip 16389 fuccofval 16826 setccofval 16939 catccofval 16957 estrccofval 16976 xpccofval 17030 psrmulr 19599 cnfldmul 19967 cnfldds 19971 trkgitv 25567 signswch 30978 algmulr 38274 clsk1indlem1 38867 rngccofvalALTV 42510 ringccofvalALTV 42573 |
Copyright terms: Public domain | W3C validator |