Theorem difss2d 4094

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

Syntax hints:   → wi 4   ∖ cdif 3903   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3909  df-ss 3923

This theorem is referenced by:  oacomf1olem  8550  numacn  10034  ramub1lem1  17087  ramub1lem2  17088  mreexexlem2d  17702  mreexexlem3d  17703  mreexexlem4d  17704  acsfiindd  18610  dpjidcl  20131  clsval2  23188  llycmpkgen2  23688  1stckgen  23692  alexsublem  24182  bcthlem3  25466  pmtrcnelor  33392  lfuhgr  35591  neibastop2lem  36852  pibt2  38044  eldioph2lem2  43475  limccog  46319  fourierdlem56  46859  fourierdlem95  46898