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

Theorem ssdifd 3724
 Description: If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is contained in (𝐵 ∖ 𝐶). Deduction form of ssdif 3723. (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 3723 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) ⊆ (𝐵𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∖ cdif 3552   ⊆ wss 3555 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-dif 3558  df-in 3562  df-ss 3569 This theorem is referenced by:  ssdif2d  3727  domunsncan  8004  fin1a2lem13  9178  seqcoll2  13187  rpnnen2lem11  14878  coprmprod  15299  mrieqv2d  16220  mrissmrid  16222  mreexexlem4d  16228  acsfiindd  17098  lsppratlem3  19068  lsppratlem4  19069  f1lindf  20080  lpss3  20858  lpcls  21078  fin1aufil  21646  rrxmval  23096  rrxmetlem  23098  uniioombllem3  23259  i1fmul  23369  itg1addlem4  23372  itg1climres  23387  limciun  23564  ig1peu  23835  ig1pdvds  23840  fusgreghash2wspv  27057  sitgclg  30185  mthmpps  31187  poimirlem11  33052  poimirlem12  33053  poimirlem15  33056  dochfln0  36246  lcfl6  36269  lcfrlem16  36327  hdmaprnlem4N  36625  caragendifcl  40035
 Copyright terms: Public domain W3C validator