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

Theorem ssdif 3311
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 3174 . . . 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 3162 . . 3  |-  ( x  e.  ( A  \  C )  <->  ( x  e.  A  /\  -.  x  e.  C ) )
4 eldif 3162 . . 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 3185 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 1684    \ cdif 3149    C_ wss 3152
This theorem is referenced by:  ssdifd  3312  domunsncan  6962  php  7045  pssnn  7081  mapfien  7399  fin1a2lem13  8038  axcclem  8083  seqcoll2  11402  isercolllem3  12140  rpnnen2lem11  12503  dprdres  15263  dpjidcl  15293  ablfac1eulem  15307  lspsnat  15898  lsppratlem3  15902  lsppratlem4  15903  lbsextlem2  15912  lbsextlem3  15913  mplmonmul  16208  cnsubdrglem  16422  lpss3  16876  lpcls  17092  clscon  17156  2ndcdisj2  17183  kqdisj  17423  fin1aufil  17627  nulmbl2  18894  uniioombllem3  18940  i1f1  19045  itg11  19046  i1fmul  19051  itg1addlem4  19054  itg1climres  19069  limcresi  19235  limciun  19244  dvreslem  19259  dvres2lem  19260  dvaddbr  19287  dvmulbr  19288  lhop  19363  ig1peu  19557  ig1pdvds  19562  elqaa  19702  xrge00  23311  lpss2  26468  divrngidl  26653  f1lindf  27292  mvdco  27388  cntzsdrg  27510  dochfln0  31667  lcfl6  31690  lcfrlem16  31748  hdmaprnlem4N  32046
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator