Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > snsstp1 | 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 |
---|---|
snsstp1 | ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snsspr1 4741 | . . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵} | |
2 | ssun1 4147 | . . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶}) | |
3 | 1, 2 | sstri 3975 | . 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶}) |
4 | df-tp 4564 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | |
5 | 3, 4 | 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-pr 4562 df-tp 4564 |
This theorem is referenced by: fr3nr 7482 rngbase 16610 srngbase 16618 lmodbase 16627 ipsbase 16634 ipssca 16637 phlbase 16644 topgrpbas 16652 otpsbas 16659 odrngbas 16670 odrngtset 16673 prdssca 16719 prdsbas 16720 prdstset 16729 imasbas 16775 imassca 16782 imastset 16785 fucbas 17220 setcbas 17328 catcbas 17347 estrcbas 17365 psrbas 20088 psrsca 20099 cnfldbas 20479 cnfldtset 20483 trkgbas 26159 signswch 31731 algbase 39658 clsk1indlem4 40274 clsk1indlem1 40275 rngcbasALTV 44152 ringcbasALTV 44215 |
Copyright terms: Public domain | W3C validator |