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 4024. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
difss2d.1 | ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶)) |
Ref | Expression |
---|---|
difss2d | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | difss2d.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶)) | |
2 | difss2 4024 | . 2 ⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → 𝐴 ⊆ 𝐵) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∖ cdif 3840 ⊆ wss 3843 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3400 df-dif 3846 df-in 3850 df-ss 3860 |
This theorem is referenced by: oacomf1olem 8223 numacn 9551 ramub1lem1 16464 ramub1lem2 16465 mreexexlem2d 17021 mreexexlem3d 17022 mreexexlem4d 17023 acsfiindd 17905 dpjidcl 19301 clsval2 21803 llycmpkgen2 22303 1stckgen 22307 alexsublem 22797 bcthlem3 24080 pmtrcnelor 30939 lfuhgr 32652 neibastop2lem 34194 pibt2 35233 eldioph2lem2 40177 limccog 42725 fourierdlem56 43267 fourierdlem95 43306 |
Copyright terms: Public domain | W3C validator |