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

Theorem sscon 3623
Description: Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.)
Assertion
Ref Expression
sscon  |-  ( A 
C_  B  ->  ( C  \  B )  C_  ( C  \  A ) )

Proof of Theorem sscon
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 ssel 3483 . . . . 5  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21con3d 133 . . . 4  |-  ( A 
C_  B  ->  ( -.  x  e.  B  ->  -.  x  e.  A
) )
32anim2d 565 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  C  /\  -.  x  e.  B
)  ->  ( x  e.  C  /\  -.  x  e.  A ) ) )
4 eldif 3471 . . 3  |-  ( x  e.  ( C  \  B )  <->  ( x  e.  C  /\  -.  x  e.  B ) )
5 eldif 3471 . . 3  |-  ( x  e.  ( C  \  A )  <->  ( x  e.  C  /\  -.  x  e.  A ) )
63, 4, 53imtr4g 270 . 2  |-  ( A 
C_  B  ->  (
x  e.  ( C 
\  B )  ->  x  e.  ( C  \  A ) ) )
76ssrdv 3495 1  |-  ( A 
C_  B  ->  ( C  \  B )  C_  ( C  \  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    e. wcel 1804    \ cdif 3458    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-dif 3464  df-in 3468  df-ss 3475
This theorem is referenced by:  sscond  3626  sorpsscmpl  6576  sbthlem1  7629  sbthlem2  7630  cantnfp1lem1  8100  cantnfp1lem3  8102  cantnfp1lem1OLD  8126  cantnfp1lem3OLD  8128  isf34lem7  8762  isf34lem6  8763  setsres  14537  mplsubglem  17967  mplsubglemOLD  17969  cctop  19380  clsval2  19424  ntrss  19429  hauscmplem  19779  ptbasin  19951  cfinfil  20267  csdfil  20268  uniioombllem5  21869  kur14lem6  28528  dvasin  30078  fourierdlem62  31840  bj-2upln1upl  34324
  Copyright terms: Public domain W3C validator