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

Theorem sscon 3637
 Description: Contraposition law for subsets. Exercise 15 of [TakeutiZaring] p. 22. (Contributed by NM, 22-Mar-1998.)
Assertion
Ref Expression
sscon

Proof of Theorem sscon
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ssel 3497 . . . . 5
21con3d 133 . . . 4
32anim2d 565 . . 3
4 eldif 3485 . . 3
5 eldif 3485 . . 3
63, 4, 53imtr4g 270 . 2
76ssrdv 3509 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  /\wa 369  e.wcel 1818  \cdif 3472  C_wss 3475 This theorem is referenced by:  sscond  3640  sorpsscmpl  6591  sbthlem1  7647  sbthlem2  7648  cantnfp1lem1  8118  cantnfp1lem3  8120  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  isf34lem7  8780  isf34lem6  8781  setsres  14660  mplsubglem  18093  mplsubglemOLD  18095  cctop  19507  clsval2  19551  ntrss  19556  hauscmplem  19906  ptbasin  20078  cfinfil  20394  csdfil  20395  uniioombllem5  21996  kur14lem6  28655  dvasin  30103  fourierdlem62  31951  bj-2upln1upl  34582 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489
 Copyright terms: Public domain W3C validator