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

Theorem sscon 3706
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 3562 . . . . 5 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21con3d 147 . . . 4 (𝐴𝐵 → (¬ 𝑥𝐵 → ¬ 𝑥𝐴))
32anim2d 587 . . 3 (𝐴𝐵 → ((𝑥𝐶 ∧ ¬ 𝑥𝐵) → (𝑥𝐶 ∧ ¬ 𝑥𝐴)))
4 eldif 3550 . . 3 (𝑥 ∈ (𝐶𝐵) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐵))
5 eldif 3550 . . 3 (𝑥 ∈ (𝐶𝐴) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐴))
63, 4, 53imtr4g 284 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐶𝐵) → 𝑥 ∈ (𝐶𝐴)))
76ssrdv 3574 1 (𝐴𝐵 → (𝐶𝐵) ⊆ (𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  wcel 1977  cdif 3537  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554
This theorem is referenced by:  sscond  3709  complss  3713  sorpsscmpl  6846  sbthlem1  7955  sbthlem2  7956  cantnfp1lem1  8458  cantnfp1lem3  8460  isf34lem7  9084  isf34lem6  9085  setsres  15729  mplsubglem  19255  cctop  20620  clsval2  20664  ntrss  20669  hauscmplem  21019  ptbasin  21190  cfinfil  21507  csdfil  21508  uniioombllem5  23161  kur14lem6  30447  bj-2upln1upl  32205  dvasin  32666  sscon34b  37337  clsk3nimkb  37358  fourierdlem62  39061  caragendifcl  39404
  Copyright terms: Public domain W3C validator