Theorem difss2d 4088

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

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

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-ss 3915

This theorem is referenced by:  oacomf1olem  8487  numacn  9949  ramub1lem1  16942  ramub1lem2  16943  mreexexlem2d  17555  mreexexlem3d  17556  mreexexlem4d  17557  acsfiindd  18463  dpjidcl  19976  clsval2  22968  llycmpkgen2  23468  1stckgen  23472  alexsublem  23962  bcthlem3  25256  pmtrcnelor  33069  lfuhgr  35185  neibastop2lem  36427  pibt2  37484  eldioph2lem2  42881  limccog  45747  fourierdlem56  46287  fourierdlem95  46326