Theorem difss2d 4090

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

Syntax hints:   → wi 4   ∖ cdif 3899   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3905  df-ss 3919

This theorem is referenced by:  oacomf1olem  8526  numacn  9998  ramub1lem1  17052  ramub1lem2  17053  mreexexlem2d  17667  mreexexlem3d  17668  mreexexlem4d  17669  acsfiindd  18575  dpjidcl  20090  clsval2  23097  llycmpkgen2  23597  1stckgen  23601  alexsublem  24091  bcthlem3  25375  pmtrcnelor  33231  lfuhgr  35428  neibastop2lem  36680  pibt2  37871  eldioph2lem2  43302  limccog  46156  fourierdlem56  46696  fourierdlem95  46735