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

Theorem ssdifd 3513
Description: If  A is contained in  B, then  ( A  \  C ) is contained in  ( B  \  C ). Deduction form of ssdif 3512. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
ssdifd.1  |-  ( ph  ->  A  C_  B )
Assertion
Ref Expression
ssdifd  |-  ( ph  ->  ( A  \  C
)  C_  ( B  \  C ) )

Proof of Theorem ssdifd
StepHypRef Expression
1 ssdifd.1 . 2  |-  ( ph  ->  A  C_  B )
2 ssdif 3512 . 2  |-  ( A 
C_  B  ->  ( A  \  C )  C_  ( B  \  C ) )
31, 2syl 16 1  |-  ( ph  ->  ( A  \  C
)  C_  ( B  \  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \ cdif 3346    C_ wss 3349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-dif 3352  df-in 3356  df-ss 3363
This theorem is referenced by:  ssdif2d  3516  domunsncan  7432  fin1a2lem13  8602  seqcoll2  12238  rpnnen2lem11  13528  mrieqv2d  14598  mrissmrid  14600  mreexexlem4d  14606  acsfiindd  15368  lsppratlem3  17252  lsppratlem4  17253  f1lindf  18273  lpss3  18770  lpcls  18990  fin1aufil  19527  rrxmval  20926  rrxmetlem  20928  uniioombllem3  21087  i1fmul  21196  itg1addlem4  21199  itg1climres  21214  limciun  21391  ig1peu  21665  ig1pdvds  21670  nbgrassovt  23368  sitgclg  26750  usgreghash2spotv  30685  dochfln0  35218  lcfl6  35241  lcfrlem16  35299  hdmaprnlem4N  35597
  Copyright terms: Public domain W3C validator