Theorem difss2d 4089

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

Syntax hints:   → wi 4   ∖ cdif 3899   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3905  df-ss 3919

This theorem is referenced by:  oacomf1olem  8479  numacn  9940  ramub1lem1  16938  ramub1lem2  16939  mreexexlem2d  17551  mreexexlem3d  17552  mreexexlem4d  17553  acsfiindd  18459  dpjidcl  19973  clsval2  22966  llycmpkgen2  23466  1stckgen  23470  alexsublem  23960  bcthlem3  25254  pmtrcnelor  33058  lfuhgr  35160  neibastop2lem  36400  pibt2  37457  eldioph2lem2  42800  limccog  45666  fourierdlem56  46206  fourierdlem95  46245