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

Theorem ssdif 3482
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 3342 . . . 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 3330 . . 3  |-  ( x  e.  ( A  \  C )  <->  ( x  e.  A  /\  -.  x  e.  C ) )
4 eldif 3330 . . 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 3354 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 3317    C_ wss 3320
This theorem is referenced by:  ssdifd  3483  php  7291  pssnn  7327  mapfien  7653  fin1a2lem13  8292  axcclem  8337  isercolllem3  12460  dprdres  15586  dpjidcl  15616  ablfac1eulem  15630  lspsnat  16217  lbsextlem2  16231  lbsextlem3  16232  mplmonmul  16527  cnsubdrglem  16749  clscon  17493  2ndcdisj2  17520  kqdisj  17764  nulmbl2  19431  i1f1  19582  itg11  19583  itg1climres  19606  limcresi  19772  dvreslem  19796  dvres2lem  19797  dvaddbr  19824  dvmulbr  19825  lhop  19900  elqaa  20239  imadifxp  24038  xrge00  24208  mblfinlem3  26245  mblfinlem4  26246  ismblfin  26247  cnambfre  26255  divrngidl  26638  mvdco  27365  cntzsdrg  27487
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-dif 3323  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator