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

Theorem sscon 3271
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
StepHypRef Expression
1 ssel 3135 . . . . 5  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21con3d 127 . . . 4  |-  ( A 
C_  B  ->  ( -.  x  e.  B  ->  -.  x  e.  A
) )
32anim2d 550 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  C  /\  -.  x  e.  B
)  ->  ( x  e.  C  /\  -.  x  e.  A ) ) )
4 eldif 3123 . . 3  |-  ( x  e.  ( C  \  B )  <->  ( x  e.  C  /\  -.  x  e.  B ) )
5 eldif 3123 . . 3  |-  ( x  e.  ( C  \  A )  <->  ( x  e.  C  /\  -.  x  e.  A ) )
63, 4, 53imtr4g 263 . 2  |-  ( A 
C_  B  ->  (
x  e.  ( C 
\  B )  ->  x  e.  ( C  \  A ) ) )
76ssrdv 3146 1  |-  ( A 
C_  B  ->  ( C  \  B )  C_  ( C  \  A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    /\ wa 360    e. wcel 1621    \ cdif 3110    C_ wss 3113
This theorem is referenced by:  sscond  3274  sorpsscmpl  6208  sbthlem1  6925  sbthlem2  6926  cantnfp1lem1  7334  cantnfp1lem3  7336  mapfien  7353  fin23lem26  7905  isf34lem7  7959  isf34lem6  7960  isercoll2  12093  setsres  13122  mplsubglem  16127  fctop  16689  cctop  16691  clsval2  16735  ntrss  16740  hauscmplem  17081  iunconlem  17101  clscon  17104  ptbasin  17220  regr1lem  17378  cfinfil  17536  csdfil  17537  blcld  17999  voliunlem1  18855  uniioombllem5  18890  kur14lem6  23100
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-dif 3116  df-in 3120  df-ss 3127
  Copyright terms: Public domain W3C validator