Theorem difss2d 4091

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

Syntax hints:   → wi 4   ∖ cdif 3898   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-ss 3918

This theorem is referenced by:  oacomf1olem  8491  numacn  9959  ramub1lem1  16954  ramub1lem2  16955  mreexexlem2d  17568  mreexexlem3d  17569  mreexexlem4d  17570  acsfiindd  18476  dpjidcl  19989  clsval2  22994  llycmpkgen2  23494  1stckgen  23498  alexsublem  23988  bcthlem3  25282  pmtrcnelor  33173  lfuhgr  35312  neibastop2lem  36554  pibt2  37622  eldioph2lem2  43003  limccog  45866  fourierdlem56  46406  fourierdlem95  46445