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

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

Proof of Theorem ssdifssd
StepHypRef Expression
1 ssdifd.1 . 2  |-  ( ph  ->  A  C_  B )
2 ssdifss 3620 . 2  |-  ( A 
C_  B  ->  ( A  \  C )  C_  B )
31, 2syl 16 1  |-  ( ph  ->  ( A  \  C
)  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \ cdif 3458    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-dif 3464  df-in 3468  df-ss 3475
This theorem is referenced by:  unblem1  7774  fin23lem26  8708  fin23lem29  8724  isf32lem8  8743  mrieqvlemd  15008  mrieqv2d  15018  mrissmrid  15020  mreexmrid  15022  mreexexlem2d  15024  mreexexlem4d  15026  acsfiindd  15786  ablfac1eulem  17102  lbspss  17707  lspsolv  17768  lsppratlem3  17774  lsppratlem4  17775  lspprat  17778  islbs2  17779  islbs3  17780  lbsextlem2  17784  lbsextlem3  17785  lbsextlem4  17786  lpss3  19623  islp3  19625  neitr  19659  restlp  19662  lpcls  19843  qtoprest  20196  ufinffr  20408  cldsubg  20587  xrge0gsumle  21316  bcthlem5  21745  rrxmval  21810  cmmbl  21923  nulmbl2  21925  shftmbl  21927  iundisj2  21937  uniiccdif  21965  uniiccmbl  21977  itg1val2  22069  itg1cl  22070  itg1ge0  22071  i1fadd  22080  itg1addlem5  22085  i1fmulc  22088  itg1mulc  22089  itg10a  22095  itg1ge0a  22096  itg1climres  22099  mbfi1fseqlem4  22103  itgss3  22199  limcdif  22258  limcnlp  22260  limcmpt2  22266  perfdvf  22285  dvcnp2  22301  dvaddbr  22319  dvmulbr  22320  dvferm1  22364  dvferm2  22366  ftc1lem6  22420  ig1peu  22550  ig1pdvds  22555  taylthlem1  22746  taylthlem2  22747  ulmdvlem3  22775  rlimcnp  23273  wilthlem2  23321  iundisj2f  27427  ofpreima2  27486  iundisj2fi  27580  eulerpartlemgs2  28297  ballotlemfrc  28443  cvmscld  28696  ftc1cnnc  30065  cntzsdrg  31127  limcrecl  31589  fperdvper  31669  stoweidlem57  31793  dirkercncflem3  31841  fourierdlem42  31885  fourierdlem46  31889  fourierdlem62  31905  lincdifsn  32895  lindslinindsimp1  32928  lincresunit3lem2  32951  lsatfixedN  34609  dochsnkr  37074  hdmaprnlem4tN  37457
  Copyright terms: Public domain W3C validator