|   | 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 4190. Partial converse of unssd 4192. (Contributed by David Moews, 1-May-2017.) | 
| Ref | Expression | 
|---|---|
| unssad.1 | ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) | 
| Ref | Expression | 
|---|---|
| unssbd | ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | unssad.1 | . . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
| 2 | unss 4190 | . . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
| 3 | 1, 2 | sylibr 234 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) | 
| 4 | 3 | simprd 495 | 1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∪ cun 3949 ⊆ wss 3951 | 
| 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 | 
| This theorem is referenced by: eldifpw 7788 naddcllem 8714 ertr 8760 finsschain 9399 r0weon 10052 ackbij1lem16 10274 wunfi 10761 wunex2 10778 hashf1lem2 14495 sumsplit 15804 fsum2dlem 15806 fsumabs 15837 fsumrlim 15847 fsumo1 15848 fsumiun 15857 fprod2dlem 16016 mreexexlem3d 17689 yonedalem1 18317 yonedalem21 18318 yonedalem3a 18319 yonedalem4c 18322 yonedalem22 18323 yonedalem3b 18324 yonedainv 18326 yonffthlem 18327 ablfac1eulem 20092 lsmsp 21085 lsppratlem3 21151 mplcoe1 22055 mdetunilem9 22626 filufint 23928 fmfnfmlem4 23965 hausflim 23989 fclsfnflim 24035 fsumcn 24894 itgfsum 25862 jensenlem1 27030 jensenlem2 27031 gsumvsca1 33232 gsumvsca2 33233 qsdrngilem 33522 evls1fldgencl 33720 fldextrspunlem1 33725 constrextdg2lem 33789 ordtconnlem1 33923 vhmcls 35571 mclsppslem 35588 rngunsnply 43181 brtrclfv2 43740 | 
| Copyright terms: Public domain | W3C validator |