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

Theorem sscond 4122
 Description: If 𝐴 is contained in 𝐵, then (𝐶 ∖ 𝐵) is contained in (𝐶 ∖ 𝐴). Deduction form of sscon 4119. (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 4119 . 2 (𝐴𝐵 → (𝐶𝐵) ⊆ (𝐶𝐴))
31, 2syl 17 1 (𝜑 → (𝐶𝐵) ⊆ (𝐶𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∖ cdif 3937   ⊆ wss 3940 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-dif 3943  df-in 3947  df-ss 3956 This theorem is referenced by:  ssdif2d  4124  eldifeldifsn  4743  fin23lem26  9736  isercoll2  15015  fctop  21528  ntrss  21579  iunconnlem  21951  clsconn  21954  regr1lem  22263  blcld  23030  rrxdstprj1  23927  voliunlem1  24066  carsgclctunlem2  31463  salexct  42483  meaiininclem  42634  carageniuncllem2  42670
 Copyright terms: Public domain W3C validator