| 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 4179 | . 2 ⊢ {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶}) | |
| 2 | df-tp 4631 | . 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶}) | |
| 3 | 1, 2 | 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-tp 4631 |
| This theorem is referenced by: fr3nr 7792 rngmulr 17345 srngmulr 17356 lmodsca 17372 ipsmulr 17383 ipsip 17386 phlsca 17393 topgrptset 17408 otpsle 17423 odrngmulr 17450 odrngds 17453 prdsmulr 17504 prdsip 17506 prdsds 17509 imasds 17558 imasmulr 17563 imasip 17566 fuccofval 18007 setccofval 18127 catccofval 18149 estrccofval 18173 xpccofval 18227 mpocnfldmul 21371 cnfldds 21376 cnfldmulOLD 21385 cnflddsOLD 21389 psrmulr 21962 trkgitv 28455 rlocmulval 33273 idlsrgmulr 33535 signswch 34576 algmulr 43188 clsk1indlem1 44058 rngccofvalALTV 48186 ringccofvalALTV 48220 mndtcco 49182 |
| Copyright terms: Public domain | W3C validator |