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

Theorem difss2d 3469
Description: If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3468. (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 3468 . 2  |-  ( A 
C_  ( B  \  C )  ->  A  C_  B )
31, 2syl 16 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \ cdif 3309    C_ wss 3312
This theorem is referenced by:  oacomf1olem  6799  numacn  7922  ramub1lem1  13386  ramub1lem2  13387  mreexexlem2d  13862  mreexexlem3d  13863  mreexexlem4d  13864  mreexexd  13865  acsfiindd  14595  dpjidcl  15608  clsval2  17106  llycmpkgen2  17574  1stckgen  17578  alexsublem  18067  bcthlem3  19271  neibastop2lem  26380  eldioph2lem2  26810
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-dif 3315  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator