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

Theorem sscon 4099
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 3938 . . . . 5 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21con3d 152 . . . 4 (𝐴𝐵 → (¬ 𝑥𝐵 → ¬ 𝑥𝐴))
32anim2d 613 . . 3 (𝐴𝐵 → ((𝑥𝐶 ∧ ¬ 𝑥𝐵) → (𝑥𝐶 ∧ ¬ 𝑥𝐴)))
4 eldif 3921 . . 3 (𝑥 ∈ (𝐶𝐵) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐵))
5 eldif 3921 . . 3 (𝑥 ∈ (𝐶𝐴) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐴))
63, 4, 53imtr4g 296 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐶𝐵) → 𝑥 ∈ (𝐶𝐴)))
76ssrdv 3951 1 (𝐴𝐵 → (𝐶𝐵) ⊆ (𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wcel 2107  cdif 3908  wss 3911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-dif 3914  df-in 3918  df-ss 3928
This theorem is referenced by:  sscond  4102  complss  4107  sscon34b  4255  sorpsscmpl  7672  sbthlem1  9030  sbthlem2  9031  cantnfp1lem1  9619  cantnfp1lem3  9621  isf34lem7  10320  isf34lem6  10321  setsres  17055  mplsubglem  21421  cctop  22372  clsval2  22417  ntrss  22422  hauscmplem  22773  ptbasin  22944  cfinfil  23260  csdfil  23261  uniioombllem5  24967  kur14lem6  33862  bj-2upln1upl  35541  dvasin  36208  clsk3nimkb  42400  fourierdlem62  44495  caragendifcl  44841
  Copyright terms: Public domain W3C validator