Theorem difss2d 4085

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

This proof depends on syntax axioms:   → wi 4   ∖ cdif 3895   ⊆ wss 3913

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3899  df-ss 3914

This theorem is used by:  oacomf1olem  8572  numacn  10128  ramub1lem1  17204  ramub1lem2  17205  mreexexlem2d  17819  mreexexlem3d  17820  mreexexlem4d  17821  acsfiindd  18727  dpjidcl  20274  clsval2  23368  llycmpkgen2  23869  1stckgen  23873  alexsublem  24363  bcthlem3  25647  lfuhgr  29726  pmtrcnelor  33652  neibastop2lem  37148  pibt2  38341  eldioph2lem2  43772  limccog  46632  fourierdlem56  47172  fourierdlem95  47211