| 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 4142. Partial converse of unssd 4144. (Contributed by David Moews, 1-May-2017.) |
| Ref | Expression |
|---|---|
| unssad.1 | ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) |
| Ref | Expression |
|---|---|
| unssad | ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | unssad.1 | . . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
| 2 | unss 4142 | . . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
| 3 | 1, 2 | sylibr 234 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) |
| 4 | 3 | simpld 494 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∪ cun 3899 ⊆ wss 3901 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1544 df-ex 1781 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-v 3442 df-un 3906 df-ss 3918 |
| This theorem is referenced by: naddcllem 8604 ersym 8647 findcard2d 9091 finsschain 9259 r0weon 9922 ackbij1lem16 10144 wunex2 10649 sumsplit 15691 fsumabs 15724 fsumiun 15744 mrieqvlemd 17552 yonedalem1 18195 yonedalem21 18196 yonedalem22 18201 yonffthlem 18205 lsmsp 21038 mplcoe1 21992 mdetunilem9 22564 ordtbas 23136 isufil2 23852 ufileu 23863 filufint 23864 fmfnfm 23902 flimclslem 23928 fclsfnflim 23971 flimfnfcls 23972 imasdsf1olem 24317 limcdif 25833 jensenlem1 26953 jensenlem2 26954 jensen 26955 gsumvsca1 33308 gsumvsca2 33309 qsdrngilem 33575 fldgenfldext 33825 evls1fldgencl 33827 fldextrspunlem1 33832 fldextrspunfld 33833 algextdeglem1 33874 algextdeglem2 33875 algextdeglem3 33876 algextdeglem4 33877 constrextdg2lem 33905 constrllcllem 33909 constrlccllem 33910 constrcccllem 33911 ordtconnlem1 34081 ssmcls 35761 mclsppslem 35777 rngunsnply 43407 mptrcllem 43850 clcnvlem 43860 brtrclfv2 43964 isotone1 44285 dvnprodlem1 46186 |
| Copyright terms: Public domain | W3C validator |