![]() |
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 4042. Partial converse of unssd 4044. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
unssad.1 | ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) |
Ref | Expression |
---|---|
unssbd | ⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unssad.1 | . . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
2 | unss 4042 | . . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
3 | 1, 2 | sylibr 226 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) |
4 | 3 | simprd 488 | 1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∪ cun 3820 ⊆ wss 3822 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2743 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-v 3410 df-un 3827 df-in 3829 df-ss 3836 |
This theorem is referenced by: eldifpw 7305 ertr 8102 finsschain 8624 r0weon 9230 ackbij1lem16 9453 wunfi 9939 wunex2 9956 hashf1lem2 13625 sumsplit 14981 fsum2dlem 14983 fsumabs 15014 fsumrlim 15024 fsumo1 15025 fsumiun 15034 fprod2dlem 15192 mreexexlem3d 16787 yonedalem1 17392 yonedalem21 17393 yonedalem3a 17394 yonedalem4c 17397 yonedalem22 17398 yonedalem3b 17399 yonedainv 17401 yonffthlem 17402 ablfac1eulem 18956 lsmsp 19592 lsppratlem3 19655 mplcoe1 19971 mdetunilem9 20948 filufint 22247 fmfnfmlem4 22284 hausflim 22308 fclsfnflim 22354 fsumcn 23196 itgfsum 24145 jensenlem1 25281 jensenlem2 25282 gsumvsca1 30557 gsumvsca2 30558 ordtconnlem1 30843 vhmcls 32370 mclsppslem 32387 rngunsnply 39207 brtrclfv2 39473 |
Copyright terms: Public domain | W3C validator |