![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > unssbd | Structured version Visualization version GIF version |
Description: If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 4182. Partial converse of unssd 4184. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
unssad.1 | ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) |
Ref | Expression |
---|---|
unssbd | ⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unssad.1 | . . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
2 | unss 4182 | . . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
3 | 1, 2 | sylibr 233 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) |
4 | 3 | simprd 494 | 1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∪ cun 3942 ⊆ wss 3944 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-v 3463 df-un 3949 df-ss 3961 |
This theorem is referenced by: eldifpw 7771 naddcllem 8697 ertr 8740 finsschain 9390 r0weon 10042 ackbij1lem16 10265 wunfi 10751 wunex2 10768 hashf1lem2 14458 sumsplit 15755 fsum2dlem 15757 fsumabs 15788 fsumrlim 15798 fsumo1 15799 fsumiun 15808 fprod2dlem 15965 mreexexlem3d 17634 yonedalem1 18272 yonedalem21 18273 yonedalem3a 18274 yonedalem4c 18277 yonedalem22 18278 yonedalem3b 18279 yonedainv 18281 yonffthlem 18282 ablfac1eulem 20046 lsmsp 20988 lsppratlem3 21054 mplcoe1 22002 mdetunilem9 22571 filufint 23873 fmfnfmlem4 23910 hausflim 23934 fclsfnflim 23980 fsumcn 24837 itgfsum 25805 jensenlem1 26969 jensenlem2 26970 gsumvsca1 33030 gsumvsca2 33031 qsdrngilem 33311 evls1fldgencl 33491 ordtconnlem1 33658 vhmcls 35309 mclsppslem 35326 rngunsnply 42741 brtrclfv2 43301 |
Copyright terms: Public domain | W3C validator |