![]() |
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 4185. Partial converse of unssd 4187. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
unssad.1 | ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) |
Ref | Expression |
---|---|
unssbd | ⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unssad.1 | . . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
2 | unss 4185 | . . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
3 | 1, 2 | sylibr 233 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) |
4 | 3 | simprd 497 | 1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∪ cun 3947 ⊆ wss 3949 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3954 df-in 3956 df-ss 3966 |
This theorem is referenced by: eldifpw 7755 naddcllem 8675 ertr 8718 finsschain 9359 r0weon 10007 ackbij1lem16 10230 wunfi 10716 wunex2 10733 hashf1lem2 14417 sumsplit 15714 fsum2dlem 15716 fsumabs 15747 fsumrlim 15757 fsumo1 15758 fsumiun 15767 fprod2dlem 15924 mreexexlem3d 17590 yonedalem1 18225 yonedalem21 18226 yonedalem3a 18227 yonedalem4c 18230 yonedalem22 18231 yonedalem3b 18232 yonedainv 18234 yonffthlem 18235 ablfac1eulem 19942 lsmsp 20697 lsppratlem3 20762 mplcoe1 21592 mdetunilem9 22122 filufint 23424 fmfnfmlem4 23461 hausflim 23485 fclsfnflim 23531 fsumcn 24386 itgfsum 25344 jensenlem1 26491 jensenlem2 26492 gsumvsca1 32371 gsumvsca2 32372 qsdrngilem 32608 algextdeglem1 32772 ordtconnlem1 32904 vhmcls 34557 mclsppslem 34574 rngunsnply 41915 brtrclfv2 42478 |
Copyright terms: Public domain | W3C validator |