![]() |
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 4185. Partial converse of unssd 4187. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
unssad.1 | ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) |
Ref | Expression |
---|---|
unssad | ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unssad.1 | . . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
2 | unss 4185 | . . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
3 | 1, 2 | sylibr 233 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) |
4 | 3 | simpld 493 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∪ cun 3945 ⊆ wss 3947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-un 3952 df-ss 3964 |
This theorem is referenced by: naddcllem 8706 ersym 8746 findcard2d 9204 finsschain 9403 r0weon 10055 ackbij1lem16 10278 wunex2 10781 sumsplit 15772 fsumabs 15805 fsumiun 15825 mrieqvlemd 17642 yonedalem1 18297 yonedalem21 18298 yonedalem22 18303 yonffthlem 18307 lsmsp 21064 mplcoe1 22044 mdetunilem9 22613 ordtbas 23187 isufil2 23903 ufileu 23914 filufint 23915 fmfnfm 23953 flimclslem 23979 fclsfnflim 24022 flimfnfcls 24023 imasdsf1olem 24370 limcdif 25896 jensenlem1 27015 jensenlem2 27016 jensen 27017 gsumvsca1 33090 gsumvsca2 33091 qsdrngilem 33369 fldgenfldext 33554 evls1fldgencl 33556 algextdeglem1 33584 algextdeglem2 33585 algextdeglem3 33586 algextdeglem4 33587 ordtconnlem1 33739 ssmcls 35395 mclsppslem 35411 rngunsnply 42834 mptrcllem 43280 clcnvlem 43290 brtrclfv2 43394 isotone1 43715 dvnprodlem1 45567 |
Copyright terms: Public domain | W3C validator |