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

Theorem sscon 3485
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 3345 . . . . 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 3333 . . 3  |-  ( x  e.  ( C  \  B )  <->  ( x  e.  C  /\  -.  x  e.  B ) )
5 eldif 3333 . . 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 3357 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 1756    \ cdif 3320    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-dif 3326  df-in 3330  df-ss 3337
This theorem is referenced by:  sscond  3488  sorpsscmpl  6366  sbthlem1  7413  sbthlem2  7414  cantnfp1lem1  7878  cantnfp1lem3  7880  cantnfp1lem1OLD  7904  cantnfp1lem3OLD  7906  isf34lem7  8540  isf34lem6  8541  setsres  14194  mplsubglem  17487  mplsubglemOLD  17489  cctop  18585  clsval2  18629  ntrss  18634  hauscmplem  18984  ptbasin  19125  cfinfil  19441  csdfil  19442  uniioombllem5  21042  kur14lem6  27051  dvasin  28433  bj-2upln1upl  32364
  Copyright terms: Public domain W3C validator