Theorem difss2d 4086

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

This proof depends on syntax axioms:   → wi 4   ∖ cdif 3896   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-ss 3916

This theorem is used by:  oacomf1olem  8556  numacn  10109  ramub1lem1  17184  ramub1lem2  17185  mreexexlem2d  17799  mreexexlem3d  17800  mreexexlem4d  17801  acsfiindd  18707  dpjidcl  20254  clsval2  23348  llycmpkgen2  23849  1stckgen  23853  alexsublem  24343  bcthlem3  25627  lfuhgr  29708  pmtrcnelor  33634  neibastop2lem  37118  pibt2  38308  eldioph2lem2  43725  limccog  46576  fourierdlem56  47116  fourierdlem95  47155