Theorem difss2d 4134

Description: If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 4133. (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 4133	. 2 ⊢ (𝐴 ⊆ (𝐵 ∖ 𝐶) → 𝐴 ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∖ cdif 3945   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951  df-in 3955  df-ss 3965

This theorem is referenced by:  oacomf1olem  8566  numacn  10046  ramub1lem1  16963  ramub1lem2  16964  mreexexlem2d  17593  mreexexlem3d  17594  mreexexlem4d  17595  acsfiindd  18510  dpjidcl  19969  clsval2  22774  llycmpkgen2  23274  1stckgen  23278  alexsublem  23768  bcthlem3  25067  pmtrcnelor  32510  lfuhgr  34394  neibastop2lem  35548  pibt2  36601  eldioph2lem2  41801  limccog  44635  fourierdlem56  45177  fourierdlem95  45216