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

Theorem sscon 3312
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 ) )
Dummy variable  x is distinct from all other variables.

Proof of Theorem sscon
StepHypRef Expression
1 ssel 3176 . . . . 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 3164 . . 3  |-  ( x  e.  ( C  \  B )  <->  ( x  e.  C  /\  -.  x  e.  B ) )
5 eldif 3164 . . 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 3187 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 1685    \ cdif 3151    C_ wss 3154
This theorem is referenced by:  sscond  3315  sorpsscmpl  6250  sbthlem1  6967  sbthlem2  6968  cantnfp1lem1  7376  cantnfp1lem3  7378  mapfien  7395  fin23lem26  7947  isf34lem7  8001  isf34lem6  8002  isercoll2  12137  setsres  13169  mplsubglem  16174  fctop  16736  cctop  16738  clsval2  16782  ntrss  16787  hauscmplem  17128  iunconlem  17148  clscon  17151  ptbasin  17267  regr1lem  17425  cfinfil  17583  csdfil  17584  blcld  18046  voliunlem1  18902  uniioombllem5  18937  kur14lem6  23147
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-dif 3157  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator