Theorem difss2d 4095

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

Syntax hints:   → wi 4   ∖ cdif 3904   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3910  df-ss 3924

This theorem is referenced by:  oacomf1olem  8537  numacn  10021  ramub1lem1  17074  ramub1lem2  17075  mreexexlem2d  17689  mreexexlem3d  17690  mreexexlem4d  17691  acsfiindd  18597  dpjidcl  20118  clsval2  23164  llycmpkgen2  23664  1stckgen  23668  alexsublem  24158  bcthlem3  25442  pmtrcnelor  33319  lfuhgr  35476  neibastop2lem  36728  pibt2  37918  eldioph2lem2  43349  limccog  46195  fourierdlem56  46735  fourierdlem95  46774