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

Theorem ssdif 3570
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 3428 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21anim1d 568 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  B  /\  -.  x  e.  C ) ) )
3 eldif 3416 . . 3  |-  ( x  e.  ( A  \  C )  <->  ( x  e.  A  /\  -.  x  e.  C ) )
4 eldif 3416 . . 3  |-  ( x  e.  ( B  \  C )  <->  ( x  e.  B  /\  -.  x  e.  C ) )
52, 3, 43imtr4g 274 . 2  |-  ( A 
C_  B  ->  (
x  e.  ( A 
\  C )  ->  x  e.  ( B  \  C ) ) )
65ssrdv 3440 1  |-  ( A 
C_  B  ->  ( A  \  C )  C_  ( B  \  C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 371    e. wcel 1889    \ cdif 3403    C_ wss 3406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-dif 3409  df-in 3413  df-ss 3420
This theorem is referenced by:  ssdifd  3571  php  7761  pssnn  7795  fin1a2lem13  8847  axcclem  8892  isercolllem3  13742  mvdco  17098  dprdres  17673  dpjidcl  17703  ablfac1eulem  17717  lspsnat  18380  lbsextlem2  18394  lbsextlem3  18395  mplmonmul  18700  cnsubdrglem  19031  clscon  20457  2ndcdisj2  20484  kqdisj  20759  nulmbl2  22502  i1f1  22660  itg11  22661  itg1climres  22684  limcresi  22852  dvreslem  22876  dvres2lem  22877  dvaddbr  22904  dvmulbr  22905  lhop  22980  elqaa  23290  difres  28223  imadifxp  28224  xrge00  28460  eulerpartlemmf  29220  eulerpartlemgf  29224  bj-2upln1upl  31630  mblfinlem3  31991  mblfinlem4  31992  ismblfin  31993  cnambfre  32001  divrngidl  32273  cntzsdrg  36080  radcnvrat  36674  fourierdlem62  38042
  Copyright terms: Public domain W3C validator