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

Theorem sscon 4143
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 3977 . . . . 5 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21con3d 152 . . . 4 (𝐴𝐵 → (¬ 𝑥𝐵 → ¬ 𝑥𝐴))
32anim2d 612 . . 3 (𝐴𝐵 → ((𝑥𝐶 ∧ ¬ 𝑥𝐵) → (𝑥𝐶 ∧ ¬ 𝑥𝐴)))
4 eldif 3961 . . 3 (𝑥 ∈ (𝐶𝐵) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐵))
5 eldif 3961 . . 3 (𝑥 ∈ (𝐶𝐴) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐴))
63, 4, 53imtr4g 296 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐶𝐵) → 𝑥 ∈ (𝐶𝐴)))
76ssrdv 3989 1 (𝐴𝐵 → (𝐶𝐵) ⊆ (𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wcel 2108  cdif 3948  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-ss 3968
This theorem is referenced by:  sscond  4146  complss  4151  sscon34b  4304  sorpsscmpl  7754  sbthlem1  9123  sbthlem2  9124  cantnfp1lem1  9718  cantnfp1lem3  9720  isf34lem7  10419  isf34lem6  10420  setsres  17215  mplsubglem  22019  cctop  23013  clsval2  23058  ntrss  23063  hauscmplem  23414  ptbasin  23585  cfinfil  23901  csdfil  23902  uniioombllem5  25622  kur14lem6  35216  bj-2upln1upl  37025  dvasin  37711  readvrec2  42391  clsk3nimkb  44053  fourierdlem62  46183  caragendifcl  46529
  Copyright terms: Public domain W3C validator