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 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-dif 3950  df-in 3954  df-ss 3964

This theorem is referenced by:  oacomf1olem  8585  numacn  10073  ramub1lem1  16995  ramub1lem2  16996  mreexexlem2d  17625  mreexexlem3d  17626  mreexexlem4d  17627  acsfiindd  18545  dpjidcl  20015  clsval2  22967  llycmpkgen2  23467  1stckgen  23471  alexsublem  23961  bcthlem3  25267  pmtrcnelor  32827  lfuhgr  34727  neibastop2lem  35844  pibt2  36896  eldioph2lem2  42181  limccog  45008  fourierdlem56  45550  fourierdlem95  45589