Theorem difss2d 4092

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

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

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 3440  df-dif 3908  df-ss 3922

This theorem is referenced by:  oacomf1olem  8489  numacn  9962  ramub1lem1  16956  ramub1lem2  16957  mreexexlem2d  17569  mreexexlem3d  17570  mreexexlem4d  17571  acsfiindd  18477  dpjidcl  19957  clsval2  22953  llycmpkgen2  23453  1stckgen  23457  alexsublem  23947  bcthlem3  25242  pmtrcnelor  33046  lfuhgr  35090  neibastop2lem  36333  pibt2  37390  eldioph2lem2  42734  limccog  45602  fourierdlem56  46144  fourierdlem95  46183