Theorem difss2d 4096

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

This proof depends on syntax axioms:   → wi 4   ∖ cdif 3905   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-dif 3911  df-ss 3925

This theorem is used by:  oacomf1olem  8558  numacn  10052  ramub1lem1  17111  ramub1lem2  17112  mreexexlem2d  17726  mreexexlem3d  17727  mreexexlem4d  17728  acsfiindd  18634  dpjidcl  20161  clsval2  23244  llycmpkgen2  23744  1stckgen  23748  alexsublem  24238  bcthlem3  25522  pmtrcnelor  33442  lfuhgr  35631  neibastop2lem  36912  pibt2  38104  eldioph2lem2  43533  limccog  46377  fourierdlem56  46917  fourierdlem95  46956