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

Theorem ssdifss 3573
Description: Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.)
Assertion
Ref Expression
ssdifss  |-  ( A 
C_  B  ->  ( A  \  C )  C_  B )

Proof of Theorem ssdifss
StepHypRef Expression
1 difss 3569 . 2  |-  ( A 
\  C )  C_  A
2 sstr 3449 . 2  |-  ( ( ( A  \  C
)  C_  A  /\  A  C_  B )  -> 
( A  \  C
)  C_  B )
31, 2mpan 668 1  |-  ( A 
C_  B  ->  ( A  \  C )  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \ cdif 3410    C_ wss 3413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3060  df-dif 3416  df-in 3420  df-ss 3427
This theorem is referenced by:  ssdifssd  3580  xrsupss  11552  xrinfmss  11553  rpnnen2  14166  lpval  19931  lpdifsn  19935  islp2  19937  lpcls  20156  mblfinlem3  31405  mblfinlem4  31406  voliunnfl  31410  ssdifcl  35602  sssymdifcl  35603  fourierdlem102  37340  fourierdlem114  37352  lindslinindimp2lem4  38554  lindslinindsimp2lem5  38555  lindslinindsimp2  38556  lincresunit3  38574
  Copyright terms: Public domain W3C validator