Theorem difss2d 4069

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

Syntax hints:   → wi 4   ∖ cdif 3884   ⊆ wss 3887

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904

This theorem is referenced by:  oacomf1olem  8395  numacn  9805  ramub1lem1  16727  ramub1lem2  16728  mreexexlem2d  17354  mreexexlem3d  17355  mreexexlem4d  17356  acsfiindd  18271  dpjidcl  19661  clsval2  22201  llycmpkgen2  22701  1stckgen  22705  alexsublem  23195  bcthlem3  24490  pmtrcnelor  31360  lfuhgr  33079  neibastop2lem  34549  pibt2  35588  eldioph2lem2  40583  limccog  43161  fourierdlem56  43703  fourierdlem95  43742