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

Theorem ssdif 3577
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 3435 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21anim1d 562 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  B  /\  -.  x  e.  C ) ) )
3 eldif 3423 . . 3  |-  ( x  e.  ( A  \  C )  <->  ( x  e.  A  /\  -.  x  e.  C ) )
4 eldif 3423 . . 3  |-  ( x  e.  ( B  \  C )  <->  ( x  e.  B  /\  -.  x  e.  C ) )
52, 3, 43imtr4g 270 . 2  |-  ( A 
C_  B  ->  (
x  e.  ( A 
\  C )  ->  x  e.  ( B  \  C ) ) )
65ssrdv 3447 1  |-  ( A 
C_  B  ->  ( A  \  C )  C_  ( B  \  C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367    e. wcel 1842    \ 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:  ssdifd  3578  php  7659  pssnn  7693  mapfienOLD  8090  fin1a2lem13  8744  axcclem  8789  isercolllem3  13545  mvdco  16686  dprdres  17287  dpjidcl  17319  dpjidclOLD  17326  ablfac1eulem  17335  lspsnat  18003  lbsextlem2  18017  lbsextlem3  18018  mplmonmul  18338  cnsubdrglem  18681  clscon  20115  2ndcdisj2  20142  kqdisj  20417  nulmbl2  22131  i1f1  22281  itg11  22282  itg1climres  22305  limcresi  22473  dvreslem  22497  dvres2lem  22498  dvaddbr  22525  dvmulbr  22526  lhop  22601  elqaa  22902  difres  27773  imadifxp  27774  xrge00  28006  eulerpartlemmf  28700  eulerpartlemgf  28704  bj-2upln1upl  31135  mblfinlem3  31406  mblfinlem4  31407  ismblfin  31408  cnambfre  31416  divrngidl  31688  cntzsdrg  35496  radcnvrat  36024  fourierdlem62  37301
  Copyright terms: Public domain W3C validator