![]() |
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 32402 gsumvsca2 32403 qsdrngilem 32639 algextdeglem1 32803 ordtconnlem1 32935 vhmcls 34588 mclsppslem 34605 rngunsnply 41963 brtrclfv2 42526 |
Copyright terms: Public domain | W3C validator |