Theorem difss2d 4076

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

Syntax hints:   → wi 4   ∖ cdif 3887   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-dif 3893  df-ss 3907

This theorem is referenced by:  oacomf1olem  8496  numacn  9969  ramub1lem1  16995  ramub1lem2  16996  mreexexlem2d  17609  mreexexlem3d  17610  mreexexlem4d  17611  acsfiindd  18517  dpjidcl  20033  clsval2  23040  llycmpkgen2  23540  1stckgen  23544  alexsublem  24034  bcthlem3  25318  pmtrcnelor  33179  lfuhgr  35353  neibastop2lem  36595  pibt2  37786  eldioph2lem2  43217  limccog  46072  fourierdlem56  46612  fourierdlem95  46651