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 4148 | . 2 ⊢ {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶}) | |
2 | df-tp 4564 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | |
3 | 1, 2 | sseqtrri 4003 | 1 ⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶} |
Colors of variables: wff setvar class |
Syntax hints: ∪ cun 3933 ⊆ wss 3935 {csn 4559 {cpr 4561 {ctp 4563 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3497 df-un 3940 df-in 3942 df-ss 3951 df-tp 4564 |
This theorem is referenced by: fr3nr 7482 rngmulr 16612 srngmulr 16620 lmodsca 16629 ipsmulr 16636 ipsip 16639 phlsca 16646 topgrptset 16654 otpsle 16661 odrngmulr 16672 odrngds 16675 prdsmulr 16722 prdsip 16724 prdsds 16727 imasds 16776 imasmulr 16781 imasip 16784 fuccofval 17219 setccofval 17332 catccofval 17350 estrccofval 17369 xpccofval 17422 psrmulr 20094 cnfldmul 20481 cnfldds 20485 trkgitv 26161 signswch 31731 algmulr 39660 clsk1indlem1 40275 rngccofvalALTV 44156 ringccofvalALTV 44219 |
Copyright terms: Public domain | W3C validator |