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

Theorem ssdif 3598
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 3457 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21anim1d 564 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  B  /\  -.  x  e.  C ) ) )
3 eldif 3445 . . 3  |-  ( x  e.  ( A  \  C )  <->  ( x  e.  A  /\  -.  x  e.  C ) )
4 eldif 3445 . . 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 3469 1  |-  ( A 
C_  B  ->  ( A  \  C )  C_  ( B  \  C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    e. wcel 1758    \ cdif 3432    C_ wss 3435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3078  df-dif 3438  df-in 3442  df-ss 3449
This theorem is referenced by:  ssdifd  3599  php  7604  pssnn  7641  mapfienOLD  8037  fin1a2lem13  8691  axcclem  8736  isercolllem3  13261  mvdco  16069  dprdres  16646  dpjidcl  16678  dpjidclOLD  16685  ablfac1eulem  16694  lspsnat  17348  lbsextlem2  17362  lbsextlem3  17363  mplmonmul  17666  cnsubdrglem  17988  clscon  19165  2ndcdisj2  19192  kqdisj  19436  nulmbl2  21150  i1f1  21300  itg11  21301  itg1climres  21324  limcresi  21492  dvreslem  21516  dvres2lem  21517  dvaddbr  21544  dvmulbr  21545  lhop  21620  elqaa  21920  imadifxp  26089  xrge00  26291  eulerpartlemmf  26901  eulerpartlemgf  26905  mblfinlem3  28577  mblfinlem4  28578  ismblfin  28579  cnambfre  28587  divrngidl  28975  cntzsdrg  29706  bj-2upln1upl  32834
  Copyright terms: Public domain W3C validator