Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > unssad | Structured version Visualization version GIF version |
Description: If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4157. Partial converse of unssd 4159. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
unssad.1 | ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) |
Ref | Expression |
---|---|
unssad | ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unssad.1 | . . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
2 | unss 4157 | . . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
3 | 1, 2 | sylibr 235 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) |
4 | 3 | simpld 495 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∪ cun 3931 ⊆ wss 3933 |
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 2790 |
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 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-un 3938 df-in 3940 df-ss 3949 |
This theorem is referenced by: ersym 8290 findcard2d 8748 finsschain 8819 r0weon 9426 ackbij1lem16 9645 wunex2 10148 sumsplit 15111 fsumabs 15144 fsumiun 15164 mrieqvlemd 16888 yonedalem1 17510 yonedalem21 17511 yonedalem22 17516 yonffthlem 17520 lsmsp 19787 mplcoe1 20174 mdetunilem9 21157 ordtbas 21728 isufil2 22444 ufileu 22455 filufint 22456 fmfnfm 22494 flimclslem 22520 fclsfnflim 22563 flimfnfcls 22564 imasdsf1olem 22910 limcdif 24401 jensenlem1 25491 jensenlem2 25492 jensen 25493 gsumvsca1 30781 gsumvsca2 30782 ordtconnlem1 31066 ssmcls 32711 mclsppslem 32727 rngunsnply 39651 mptrcllem 39851 clcnvlem 39861 brtrclfv2 39950 isotone1 40276 dvnprodlem1 42107 |
Copyright terms: Public domain | W3C validator |