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

Theorem ssdif 3426
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 3286 . . . 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 3274 . . 3  |-  ( x  e.  ( A  \  C )  <->  ( x  e.  A  /\  -.  x  e.  C ) )
4 eldif 3274 . . 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 3298 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 1717    \ cdif 3261    C_ wss 3264
This theorem is referenced by:  ssdifd  3427  php  7228  pssnn  7264  mapfien  7587  fin1a2lem13  8226  axcclem  8271  isercolllem3  12388  dprdres  15514  dpjidcl  15544  ablfac1eulem  15558  lspsnat  16145  lbsextlem2  16159  lbsextlem3  16160  mplmonmul  16455  cnsubdrglem  16673  clscon  17415  2ndcdisj2  17442  kqdisj  17686  nulmbl2  19299  i1f1  19450  itg11  19451  itg1climres  19474  limcresi  19640  dvreslem  19664  dvres2lem  19665  dvaddbr  19692  dvmulbr  19693  lhop  19768  elqaa  20107  imadifxp  23882  xrge00  24038  divrngidl  26330  mvdco  27058  cntzsdrg  27180
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-dif 3267  df-in 3271  df-ss 3278
  Copyright terms: Public domain W3C validator