Theorem difss2d 4149

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

Syntax hints:   → wi 4   ∖ cdif 3960   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-dif 3966  df-ss 3980

This theorem is referenced by:  oacomf1olem  8601  numacn  10087  ramub1lem1  17060  ramub1lem2  17061  mreexexlem2d  17690  mreexexlem3d  17691  mreexexlem4d  17692  acsfiindd  18611  dpjidcl  20093  clsval2  23074  llycmpkgen2  23574  1stckgen  23578  alexsublem  24068  bcthlem3  25374  pmtrcnelor  33094  lfuhgr  35102  neibastop2lem  36343  pibt2  37400  eldioph2lem2  42749  limccog  45576  fourierdlem56  46118  fourierdlem95  46157