Theorem difss2d 4102

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

Syntax hints:   → wi 4   ∖ cdif 3911   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-ss 3931

This theorem is referenced by:  oacomf1olem  8528  numacn  10002  ramub1lem1  16997  ramub1lem2  16998  mreexexlem2d  17606  mreexexlem3d  17607  mreexexlem4d  17608  acsfiindd  18512  dpjidcl  19990  clsval2  22937  llycmpkgen2  23437  1stckgen  23441  alexsublem  23931  bcthlem3  25226  pmtrcnelor  33048  lfuhgr  35105  neibastop2lem  36348  pibt2  37405  eldioph2lem2  42749  limccog  45618  fourierdlem56  46160  fourierdlem95  46199