Theorem difss2d 4062

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

Syntax hints:   → wi 4   ∖ cdif 3878   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898

This theorem is referenced by:  oacomf1olem  8173  numacn  9460  ramub1lem1  16352  ramub1lem2  16353  mreexexlem2d  16908  mreexexlem3d  16909  mreexexlem4d  16910  acsfiindd  17779  dpjidcl  19173  clsval2  21655  llycmpkgen2  22155  1stckgen  22159  alexsublem  22649  bcthlem3  23930  pmtrcnelor  30785  lfuhgr  32477  neibastop2lem  33821  pibt2  34834  eldioph2lem2  39702  limccog  42262  fourierdlem56  42804  fourierdlem95  42843