Theorem difss2d 4065

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

Syntax hints:   → wi 4   ∖ cdif 3880   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900

This theorem is referenced by:  oacomf1olem  8357  numacn  9736  ramub1lem1  16655  ramub1lem2  16656  mreexexlem2d  17271  mreexexlem3d  17272  mreexexlem4d  17273  acsfiindd  18186  dpjidcl  19576  clsval2  22109  llycmpkgen2  22609  1stckgen  22613  alexsublem  23103  bcthlem3  24395  pmtrcnelor  31262  lfuhgr  32979  neibastop2lem  34476  pibt2  35515  eldioph2lem2  40499  limccog  43051  fourierdlem56  43593  fourierdlem95  43632