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

Theorem ssdif 3324
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 3187 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21anim1d 547 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  B  /\  -.  x  e.  C ) ) )
3 eldif 3175 . . 3  |-  ( x  e.  ( A  \  C )  <->  ( x  e.  A  /\  -.  x  e.  C ) )
4 eldif 3175 . . 3  |-  ( x  e.  ( B  \  C )  <->  ( x  e.  B  /\  -.  x  e.  C ) )
52, 3, 43imtr4g 261 . 2  |-  ( A 
C_  B  ->  (
x  e.  ( A 
\  C )  ->  x  e.  ( B  \  C ) ) )
65ssrdv 3198 1  |-  ( A 
C_  B  ->  ( A  \  C )  C_  ( B  \  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    e. wcel 1696    \ cdif 3162    C_ wss 3165
This theorem is referenced by:  ssdifd  3325  domunsncan  6978  php  7061  pssnn  7097  mapfien  7415  fin1a2lem13  8054  axcclem  8099  seqcoll2  11418  isercolllem3  12156  rpnnen2lem11  12519  dprdres  15279  dpjidcl  15309  ablfac1eulem  15323  lspsnat  15914  lsppratlem3  15918  lsppratlem4  15919  lbsextlem2  15928  lbsextlem3  15929  mplmonmul  16224  cnsubdrglem  16438  lpss3  16892  lpcls  17108  clscon  17172  2ndcdisj2  17199  kqdisj  17439  fin1aufil  17643  nulmbl2  18910  uniioombllem3  18956  i1f1  19061  itg11  19062  i1fmul  19067  itg1addlem4  19070  itg1climres  19085  limcresi  19251  limciun  19260  dvreslem  19275  dvres2lem  19276  dvaddbr  19303  dvmulbr  19304  lhop  19379  ig1peu  19573  ig1pdvds  19578  elqaa  19718  xrge00  23326  lpss2  26571  divrngidl  26756  f1lindf  27395  mvdco  27491  cntzsdrg  27613  dochfln0  32289  lcfl6  32312  lcfrlem16  32370  hdmaprnlem4N  32668
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator