![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > unssad | Structured version Visualization version GIF version |
Description: If (𝐴 ∪ 𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4009. Partial converse of unssd 4011. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
unssad.1 | ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) |
Ref | Expression |
---|---|
unssad | ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unssad.1 | . . 3 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
2 | unss 4009 | . . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶) | |
3 | 1, 2 | sylibr 226 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶)) |
4 | 3 | simpld 490 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∪ cun 3789 ⊆ wss 3791 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-ext 2753 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-v 3399 df-un 3796 df-in 3798 df-ss 3805 |
This theorem is referenced by: ersym 8038 findcard2d 8490 finsschain 8561 r0weon 9168 ackbij1lem16 9392 wunex2 9895 sumsplit 14904 fsumabs 14937 fsumiun 14957 mrieqvlemd 16675 yonedalem1 17298 yonedalem21 17299 yonedalem22 17304 yonffthlem 17308 lsmsp 19481 mplcoe1 19862 mdetunilem9 20831 ordtbas 21404 isufil2 22120 ufileu 22131 filufint 22132 fmfnfm 22170 flimclslem 22196 fclsfnflim 22239 flimfnfcls 22240 imasdsf1olem 22586 limcdif 24077 jensenlem1 25165 jensenlem2 25166 jensen 25167 gsumvsca1 30344 gsumvsca2 30345 ordtconnlem1 30568 ssmcls 32063 mclsppslem 32079 rngunsnply 38684 mptrcllem 38859 clcnvlem 38869 brtrclfv2 38958 isotone1 39284 dvnprodlem1 41071 |
Copyright terms: Public domain | W3C validator |