Theorem difss2d 4162

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

Syntax hints:   → wi 4   ∖ cdif 3973   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-ss 3993

This theorem is referenced by:  oacomf1olem  8620  numacn  10118  ramub1lem1  17073  ramub1lem2  17074  mreexexlem2d  17703  mreexexlem3d  17704  mreexexlem4d  17705  acsfiindd  18623  dpjidcl  20102  clsval2  23079  llycmpkgen2  23579  1stckgen  23583  alexsublem  24073  bcthlem3  25379  pmtrcnelor  33084  lfuhgr  35085  neibastop2lem  36326  pibt2  37383  eldioph2lem2  42717  limccog  45541  fourierdlem56  46083  fourierdlem95  46122