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

Theorem sscond 4139
Description: If 𝐴 is contained in 𝐵, then (𝐶𝐵) is contained in (𝐶𝐴). Deduction form of sscon 4136. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
ssdifd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
sscond (𝜑 → (𝐶𝐵) ⊆ (𝐶𝐴))

Proof of Theorem sscond
StepHypRef Expression
1 ssdifd.1 . 2 (𝜑𝐴𝐵)
2 sscon 4136 . 2 (𝐴𝐵 → (𝐶𝐵) ⊆ (𝐶𝐴))
31, 2syl 17 1 (𝜑 → (𝐶𝐵) ⊆ (𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3943  wss 3946
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 3477  df-dif 3949  df-in 3953  df-ss 3963
This theorem is referenced by:  ssdif2d  4141  eldifeldifsn  4812  fin23lem26  10315  isercoll2  15610  fctop  22488  ntrss  22540  iunconnlem  22912  clsconn  22915  regr1lem  23224  blcld  23995  rrxdstprj1  24907  voliunlem1  25048  elrspunidl  32503  carsgclctunlem2  33255  salexct  44984  meaiininclem  45136  carageniuncllem2  45172  seposep  47459
  Copyright terms: Public domain W3C validator