Theorem difss2d 3740

Description: If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3739. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
difss2d.1	|- ( ph -> A C_ ( B \ C ) )

Assertion

Ref	Expression
difss2d	|- ( ph -> A C_ B )

Proof of Theorem difss2d

Step	Hyp	Ref	Expression
1		difss2d.1	. 2 |- ( ph -> A C_ ( B \ C ) )
2		difss2 3739	. 2 |- ( A C_ ( B \ C ) -> A C_ B )
3	1, 2	syl 17	1 |- ( ph -> A C_ B )

Syntax hints:   -> wi 4   \ cdif 3571   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588

This theorem is referenced by:  oacomf1olem  7644  numacn  8872  ramub1lem1  15730  ramub1lem2  15731  mreexexlem2d  16305  mreexexlem3d  16306  mreexexlem4d  16307  mreexexdOLD  16309  acsfiindd  17177  dpjidcl  18457  clsval2  20854  llycmpkgen2  21353  1stckgen  21357  alexsublem  21848  bcthlem3  23123  neibastop2lem  32355  eldioph2lem2  37324  limccog  39852  fourierdlem56  40379  fourierdlem95  40418