Theorem difss2d 4099

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

Syntax hints:   → wi 4   ∖ cdif 3921   ⊆ wss 3924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3488  df-dif 3927  df-in 3931  df-ss 3940

This theorem is referenced by:  oacomf1olem  8176  numacn  9461  ramub1lem1  16345  ramub1lem2  16346  mreexexlem2d  16899  mreexexlem3d  16900  mreexexlem4d  16901  acsfiindd  17770  dpjidcl  19163  clsval2  21641  llycmpkgen2  22141  1stckgen  22145  alexsublem  22635  bcthlem3  23912  pmtrcnelor  30742  lfuhgr  32371  neibastop2lem  33715  pibt2  34714  eldioph2lem2  39450  limccog  41991  fourierdlem56  42537  fourierdlem95  42576