Theorem difss2d 4121

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

Syntax hints:   → wi 4   ∖ cdif 3930   ⊆ wss 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3466  df-dif 3936  df-ss 3950

This theorem is referenced by:  oacomf1olem  8585  numacn  10072  ramub1lem1  17047  ramub1lem2  17048  mreexexlem2d  17664  mreexexlem3d  17665  mreexexlem4d  17666  acsfiindd  18572  dpjidcl  20051  clsval2  23023  llycmpkgen2  23523  1stckgen  23527  alexsublem  24017  bcthlem3  25315  pmtrcnelor  33057  lfuhgr  35064  neibastop2lem  36302  pibt2  37359  eldioph2lem2  42717  limccog  45580  fourierdlem56  46122  fourierdlem95  46161