Theorem difss2d 4075

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

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

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-ss 3896  df-dif 4047

This theorem is used by:  oacomf1olem  8576  numacn  10132  ramub1lem1  17210  ramub1lem2  17211  mreexexlem2d  17825  mreexexlem3d  17826  mreexexlem4d  17827  acsfiindd  18733  dpjidcl  20280  clsval2  23374  llycmpkgen2  23875  1stckgen  23879  alexsublem  24369  bcthlem3  25653  lfuhgr  29732  pmtrcnelor  33699  neibastop2lem  37241  pibt2  38434  eldioph2lem2  43866  limccog  46726  fourierdlem56  47266  fourierdlem95  47305