Theorem difss2d 4119

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

Syntax hints:   → wi 4   ∖ cdif 3928   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-dif 3934  df-ss 3948

This theorem is referenced by:  oacomf1olem  8581  numacn  10068  ramub1lem1  17051  ramub1lem2  17052  mreexexlem2d  17662  mreexexlem3d  17663  mreexexlem4d  17664  acsfiindd  18568  dpjidcl  20046  clsval2  22993  llycmpkgen2  23493  1stckgen  23497  alexsublem  23987  bcthlem3  25283  pmtrcnelor  33107  lfuhgr  35145  neibastop2lem  36383  pibt2  37440  eldioph2lem2  42759  limccog  45629  fourierdlem56  46171  fourierdlem95  46210