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

Theorem sscon 3310
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 3174 . . . . 5  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21con3d 125 . . . 4  |-  ( A 
C_  B  ->  ( -.  x  e.  B  ->  -.  x  e.  A
) )
32anim2d 548 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  C  /\  -.  x  e.  B
)  ->  ( x  e.  C  /\  -.  x  e.  A ) ) )
4 eldif 3162 . . 3  |-  ( x  e.  ( C  \  B )  <->  ( x  e.  C  /\  -.  x  e.  B ) )
5 eldif 3162 . . 3  |-  ( x  e.  ( C  \  A )  <->  ( x  e.  C  /\  -.  x  e.  A ) )
63, 4, 53imtr4g 261 . 2  |-  ( A 
C_  B  ->  (
x  e.  ( C 
\  B )  ->  x  e.  ( C  \  A ) ) )
76ssrdv 3185 1  |-  ( A 
C_  B  ->  ( C  \  B )  C_  ( C  \  A ) )
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:  sscond  3313  sorpsscmpl  6288  sbthlem1  6971  sbthlem2  6972  cantnfp1lem1  7380  cantnfp1lem3  7382  mapfien  7399  fin23lem26  7951  isf34lem7  8005  isf34lem6  8006  isercoll2  12142  setsres  13174  mplsubglem  16179  fctop  16741  cctop  16743  clsval2  16787  ntrss  16792  hauscmplem  17133  iunconlem  17153  clscon  17156  ptbasin  17272  regr1lem  17430  cfinfil  17588  csdfil  17589  blcld  18051  voliunlem1  18907  uniioombllem5  18942  kur14lem6  23742  dvreasin  24923
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