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

Theorem sscon 3624
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 3483 . . . . 5  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21con3d 133 . . . 4  |-  ( A 
C_  B  ->  ( -.  x  e.  B  ->  -.  x  e.  A
) )
32anim2d 563 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  C  /\  -.  x  e.  B
)  ->  ( x  e.  C  /\  -.  x  e.  A ) ) )
4 eldif 3471 . . 3  |-  ( x  e.  ( C  \  B )  <->  ( x  e.  C  /\  -.  x  e.  B ) )
5 eldif 3471 . . 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 3495 1  |-  ( A 
C_  B  ->  ( C  \  B )  C_  ( C  \  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367    e. wcel 1823    \ cdif 3458    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-dif 3464  df-in 3468  df-ss 3475
This theorem is referenced by:  sscond  3627  sorpsscmpl  6564  sbthlem1  7620  sbthlem2  7621  cantnfp1lem1  8088  cantnfp1lem3  8090  cantnfp1lem1OLD  8114  cantnfp1lem3OLD  8116  isf34lem7  8750  isf34lem6  8751  setsres  14746  mplsubglem  18288  mplsubglemOLD  18290  cctop  19674  clsval2  19718  ntrss  19723  hauscmplem  20073  ptbasin  20244  cfinfil  20560  csdfil  20561  uniioombllem5  22162  kur14lem6  28919  dvasin  30343  fourierdlem62  32190  bj-2upln1upl  34983
  Copyright terms: Public domain W3C validator