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 4163. Partial converse of unssd 4165. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
unssad.1 | ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) |
Ref | Expression |
---|---|
unssbd | ⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unssad.1 | . . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
2 | unss 4163 | . . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
3 | 1, 2 | sylibr 236 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) |
4 | 3 | simprd 498 | 1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∪ cun 3937 ⊆ wss 3939 |
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 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-v 3499 df-un 3944 df-in 3946 df-ss 3955 |
This theorem is referenced by: eldifpw 7493 ertr 8307 finsschain 8834 r0weon 9441 ackbij1lem16 9660 wunfi 10146 wunex2 10163 hashf1lem2 13817 sumsplit 15126 fsum2dlem 15128 fsumabs 15159 fsumrlim 15169 fsumo1 15170 fsumiun 15179 fprod2dlem 15337 mreexexlem3d 16920 yonedalem1 17525 yonedalem21 17526 yonedalem3a 17527 yonedalem4c 17530 yonedalem22 17531 yonedalem3b 17532 yonedainv 17534 yonffthlem 17535 ablfac1eulem 19197 lsmsp 19861 lsppratlem3 19924 mplcoe1 20249 mdetunilem9 21232 filufint 22531 fmfnfmlem4 22568 hausflim 22592 fclsfnflim 22638 fsumcn 23481 itgfsum 24430 jensenlem1 25567 jensenlem2 25568 gsumvsca1 30858 gsumvsca2 30859 ordtconnlem1 31171 vhmcls 32817 mclsppslem 32834 rngunsnply 39779 brtrclfv2 40078 |
Copyright terms: Public domain | W3C validator |