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

Theorem ssdif 3474
Description: Difference law for subsets. (Contributed by NM, 28-May-1998.)
Assertion
Ref Expression
ssdif  |-  ( A 
C_  B  ->  ( A  \  C )  C_  ( B  \  C ) )

Proof of Theorem ssdif
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 ssel 3334 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21anim1d 548 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  B  /\  -.  x  e.  C ) ) )
3 eldif 3322 . . 3  |-  ( x  e.  ( A  \  C )  <->  ( x  e.  A  /\  -.  x  e.  C ) )
4 eldif 3322 . . 3  |-  ( x  e.  ( B  \  C )  <->  ( x  e.  B  /\  -.  x  e.  C ) )
52, 3, 43imtr4g 262 . 2  |-  ( A 
C_  B  ->  (
x  e.  ( A 
\  C )  ->  x  e.  ( B  \  C ) ) )
65ssrdv 3346 1  |-  ( A 
C_  B  ->  ( A  \  C )  C_  ( B  \  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359    e. wcel 1725    \ cdif 3309    C_ wss 3312
This theorem is referenced by:  ssdifd  3475  php  7282  pssnn  7318  mapfien  7642  fin1a2lem13  8281  axcclem  8326  isercolllem3  12448  dprdres  15574  dpjidcl  15604  ablfac1eulem  15618  lspsnat  16205  lbsextlem2  16219  lbsextlem3  16220  mplmonmul  16515  cnsubdrglem  16737  clscon  17481  2ndcdisj2  17508  kqdisj  17752  nulmbl2  19419  i1f1  19570  itg11  19571  itg1climres  19594  limcresi  19760  dvreslem  19784  dvres2lem  19785  dvaddbr  19812  dvmulbr  19813  lhop  19888  elqaa  20227  imadifxp  24026  xrge00  24196  mblfinlem2  26191  mblfinlem3  26192  ismblfin  26193  cnambfre  26201  divrngidl  26575  mvdco  27303  cntzsdrg  27425
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