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

Theorem sscon 4135
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 3970 . . . . 5 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21con3d 152 . . . 4 (𝐴𝐵 → (¬ 𝑥𝐵 → ¬ 𝑥𝐴))
32anim2d 610 . . 3 (𝐴𝐵 → ((𝑥𝐶 ∧ ¬ 𝑥𝐵) → (𝑥𝐶 ∧ ¬ 𝑥𝐴)))
4 eldif 3954 . . 3 (𝑥 ∈ (𝐶𝐵) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐵))
5 eldif 3954 . . 3 (𝑥 ∈ (𝐶𝐴) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐴))
63, 4, 53imtr4g 295 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐶𝐵) → 𝑥 ∈ (𝐶𝐴)))
76ssrdv 3982 1 (𝐴𝐵 → (𝐶𝐵) ⊆ (𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  wcel 2098  cdif 3941  wss 3944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-dif 3947  df-ss 3961
This theorem is referenced by:  sscond  4138  complss  4143  sscon34b  4293  sorpsscmpl  7740  sbthlem1  9108  sbthlem2  9109  cantnfp1lem1  9703  cantnfp1lem3  9705  isf34lem7  10404  isf34lem6  10405  setsres  17150  mplsubglem  21961  cctop  22953  clsval2  22998  ntrss  23003  hauscmplem  23354  ptbasin  23525  cfinfil  23841  csdfil  23842  uniioombllem5  25560  kur14lem6  34949  bj-2upln1upl  36631  dvasin  37305  clsk3nimkb  43609  fourierdlem62  45691  caragendifcl  46037
  Copyright terms: Public domain W3C validator