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

Theorem sscon 3323
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 3187 . . . . 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 3175 . . 3  |-  ( x  e.  ( C  \  B )  <->  ( x  e.  C  /\  -.  x  e.  B ) )
5 eldif 3175 . . 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 3198 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 1696    \ cdif 3162    C_ wss 3165
This theorem is referenced by:  sscond  3326  sorpsscmpl  6304  sbthlem1  6987  sbthlem2  6988  cantnfp1lem1  7396  cantnfp1lem3  7398  mapfien  7415  fin23lem26  7967  isf34lem7  8021  isf34lem6  8022  isercoll2  12158  setsres  13190  mplsubglem  16195  fctop  16757  cctop  16759  clsval2  16803  ntrss  16808  hauscmplem  17149  iunconlem  17169  clscon  17172  ptbasin  17288  regr1lem  17446  cfinfil  17604  csdfil  17605  blcld  18067  voliunlem1  18923  uniioombllem5  18958  kur14lem6  23757  dvreasin  25026
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator