Theorem difss2d 4025

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.)

Hypothesis

Ref	Expression
difss2d.1	⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶))

Assertion

Ref	Expression
difss2d	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Proof of Theorem difss2d

Step	Hyp	Ref	Expression
1		difss2d.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∖ 𝐶))
2		difss2 4024	. 2 ⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → 𝐴 ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

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