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

Theorem ssdifd 3944
Description: If 𝐴 is contained in 𝐵, then (𝐴𝐶) is contained in (𝐵𝐶). Deduction form of ssdif 3943. (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 3943 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3766  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-v 3387  df-dif 3772  df-in 3776  df-ss 3783
This theorem is referenced by:  ssdif2d  3947  domunsncan  8302  fin1a2lem13  9522  seqcoll2  13498  rpnnen2lem11  15289  coprmprod  15709  mrieqv2d  16614  mrissmrid  16616  mreexexlem4d  16622  acsfiindd  17492  lsppratlem3  19472  lsppratlem4  19473  f1lindf  20486  lpss3  21277  lpcls  21497  fin1aufil  22064  rrxmval  23527  rrxmetlem  23529  uniioombllem3  23693  i1fmul  23804  itg1addlem4  23807  itg1climres  23822  limciun  23999  ig1peu  24272  ig1pdvds  24277  fusgreghash2wspv  27684  indsumin  30600  sitgclg  30920  mthmpps  31996  poimirlem11  33909  poimirlem12  33910  poimirlem15  33913  dochfln0  37498  lcfl6  37521  lcfrlem16  37579  hdmaprnlem4N  37874  caragendifcl  41474
  Copyright terms: Public domain W3C validator