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

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

Proof of Theorem ssdifd
StepHypRef Expression
1 ssdifd.1 . 2 (𝜑𝐴𝐵)
2 ssdif 4095 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) ⊆ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∖ cdif 3910   ⊆ wss 3913 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2792 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-v 3475  df-dif 3916  df-in 3920  df-ss 3930 This theorem is referenced by:  ssdif2d  4099  domunsncan  8595  fin1a2lem13  9812  seqcoll2  13808  rpnnen2lem11  15557  coprmprod  15983  mrieqv2d  16889  mrissmrid  16891  mreexexlem4d  16897  acsfiindd  17766  subdrgint  19558  lsppratlem3  19897  lsppratlem4  19898  f1lindf  20942  lpss3  21728  lpcls  21948  fin1aufil  22516  rrxmval  23988  rrxmetlem  23990  uniioombllem3  24168  i1fmul  24279  itg1addlem4  24282  itg1climres  24297  limciun  24476  ig1peu  24751  ig1pdvds  24756  fusgreghash2wspv  28099  pmtrcnel2  30742  pmtrcnelor  30743  tocyccntz  30794  indsumin  31289  sitgclg  31608  mthmpps  32837  poimirlem11  34944  poimirlem12  34945  poimirlem15  34948  dochfln0  38649  lcfl6  38672  lcfrlem16  38730  hdmaprnlem4N  39025  caragendifcl  42944
 Copyright terms: Public domain W3C validator