Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > difss2d | Structured version Visualization version GIF version |
Description: If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 4068. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
difss2d.1 | ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶)) |
Ref | Expression |
---|---|
difss2d | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | difss2d.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶)) | |
2 | difss2 4068 | . 2 ⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → 𝐴 ⊆ 𝐵) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∖ cdif 3884 ⊆ wss 3887 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-dif 3890 df-in 3894 df-ss 3904 |
This theorem is referenced by: oacomf1olem 8395 numacn 9805 ramub1lem1 16727 ramub1lem2 16728 mreexexlem2d 17354 mreexexlem3d 17355 mreexexlem4d 17356 acsfiindd 18271 dpjidcl 19661 clsval2 22201 llycmpkgen2 22701 1stckgen 22705 alexsublem 23195 bcthlem3 24490 pmtrcnelor 31360 lfuhgr 33079 neibastop2lem 34549 pibt2 35588 eldioph2lem2 40583 limccog 43161 fourierdlem56 43703 fourierdlem95 43742 |
Copyright terms: Public domain | W3C validator |