MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difss2d Structured version   Unicode version

Theorem difss2d 3601
Description: If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3600. (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
StepHypRef Expression
1 difss2d.1 . 2  |-  ( ph  ->  A  C_  ( B  \  C ) )
2 difss2 3600 . 2  |-  ( A 
C_  ( B  \  C )  ->  A  C_  B )
31, 2syl 17 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \ cdif 3439    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-dif 3445  df-in 3449  df-ss 3456
This theorem is referenced by:  oacomf1olem  7273  numacn  8478  ramub1lem1  14947  ramub1lem2  14948  mreexexlem2d  15506  mreexexlem3d  15507  mreexexlem4d  15508  mreexexd  15509  acsfiindd  16378  dpjidcl  17630  clsval2  20000  llycmpkgen2  20500  1stckgen  20504  alexsublem  20994  bcthlem3  22191  neibastop2lem  30809  eldioph2lem2  35323  limccog  37287  fourierdlem56  37609  fourierdlem95  37648
  Copyright terms: Public domain W3C validator