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

Theorem sscond 4047
 Description: If 𝐴 is contained in 𝐵, then (𝐶 ∖ 𝐵) is contained in (𝐶 ∖ 𝐴). Deduction form of sscon 4044. (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 4044 . 2 (𝐴𝐵 → (𝐶𝐵) ⊆ (𝐶𝐴))
31, 2syl 17 1 (𝜑 → (𝐶𝐵) ⊆ (𝐶𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∖ cdif 3855   ⊆ wss 3858 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-dif 3861  df-in 3865  df-ss 3875 This theorem is referenced by:  ssdif2d  4049  eldifeldifsn  4701  fin23lem26  9785  isercoll2  15073  fctop  21704  ntrss  21755  iunconnlem  22127  clsconn  22130  regr1lem  22439  blcld  23207  rrxdstprj1  24109  voliunlem1  24250  elrspunidl  31127  carsgclctunlem2  31805  salexct  43362  meaiininclem  43513  carageniuncllem2  43549
 Copyright terms: Public domain W3C validator