Theorem difss2d 4113

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

Syntax hints:   → wi 4   ∖ cdif 3935   ⊆ wss 3938

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-dif 3941  df-in 3945  df-ss 3954

This theorem is referenced by:  oacomf1olem  8192  numacn  9477  ramub1lem1  16364  ramub1lem2  16365  mreexexlem2d  16918  mreexexlem3d  16919  mreexexlem4d  16920  acsfiindd  17789  dpjidcl  19182  clsval2  21660  llycmpkgen2  22160  1stckgen  22164  alexsublem  22654  bcthlem3  23931  pmtrcnelor  30737  lfuhgr  32366  neibastop2lem  33710  pibt2  34700  eldioph2lem2  39365  limccog  41908  fourierdlem56  42454  fourierdlem95  42493