Theorem difss2d 4133

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

Syntax hints:   → wi 4   ∖ cdif 3944   ⊆ wss 3947

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3950  df-in 3954  df-ss 3964

This theorem is referenced by:  oacomf1olem  8560  numacn  10040  ramub1lem1  16955  ramub1lem2  16956  mreexexlem2d  17585  mreexexlem3d  17586  mreexexlem4d  17587  acsfiindd  18502  dpjidcl  19922  clsval2  22545  llycmpkgen2  23045  1stckgen  23049  alexsublem  23539  bcthlem3  24834  pmtrcnelor  32239  lfuhgr  34096  neibastop2lem  35233  pibt2  36286  eldioph2lem2  41484  limccog  44322  fourierdlem56  44864  fourierdlem95  44903