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

Theorem sscond 4140
Description: If 𝐴 is contained in 𝐵, then (𝐶𝐵) is contained in (𝐶𝐴). Deduction form of sscon 4137. (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 4137 . 2 (𝐴𝐵 → (𝐶𝐵) ⊆ (𝐶𝐴))
31, 2syl 17 1 (𝜑 → (𝐶𝐵) ⊆ (𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3944  wss 3947
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-dif 3950  df-in 3954  df-ss 3964
This theorem is referenced by:  ssdif2d  4142  eldifeldifsn  4813  fin23lem26  10322  isercoll2  15619  fctop  22727  ntrss  22779  iunconnlem  23151  clsconn  23154  regr1lem  23463  blcld  24234  rrxdstprj1  25157  voliunlem1  25299  elrspunidl  32820  carsgclctunlem2  33616  salexct  45348  meaiininclem  45500  carageniuncllem2  45536  seposep  47645
  Copyright terms: Public domain W3C validator