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

Theorem ssdifssd 3637
Description: If  A is contained in  B, then  ( A  \  C ) is also contained in  B. Deduction form of ssdifss 3630. (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 3630 . 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 3468    C_ wss 3471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-v 3110  df-dif 3474  df-in 3478  df-ss 3485
This theorem is referenced by:  unblem1  7763  fin23lem26  8696  fin23lem29  8712  isf32lem8  8731  mrieqvlemd  14875  mrieqv2d  14885  mrissmrid  14887  mreexmrid  14889  mreexexlem2d  14891  mreexexlem4d  14893  acsfiindd  15655  ablfac1eulem  16908  lbspss  17506  lspsolv  17567  lsppratlem3  17573  lsppratlem4  17574  lspprat  17577  islbs2  17578  islbs3  17579  lbsextlem2  17583  lbsextlem3  17584  lbsextlem4  17585  lpss3  19406  neitr  19442  restlp  19445  lpcls  19626  qtoprest  19948  ufinffr  20160  cldsubg  20339  xrge0gsumle  21068  bcthlem5  21497  rrxmval  21562  cmmbl  21675  nulmbl2  21677  shftmbl  21679  iundisj2  21689  uniiccdif  21717  uniiccmbl  21729  itg1val2  21821  itg1cl  21822  itg1ge0  21823  i1fadd  21832  itg1addlem5  21837  i1fmulc  21840  itg1mulc  21841  itg10a  21847  itg1ge0a  21848  itg1climres  21851  mbfi1fseqlem4  21855  itgss3  21951  limcdif  22010  limcnlp  22012  limcmpt2  22018  perfdvf  22037  dvcnp2  22053  dvaddbr  22071  dvmulbr  22072  dvferm1  22116  dvferm2  22118  ftc1lem6  22172  ig1peu  22302  ig1pdvds  22307  taylthlem1  22497  taylthlem2  22498  ulmdvlem3  22526  rlimcnp  23018  wilthlem2  23066  iundisj2f  27110  iundisj2fi  27258  eulerpartlemgs2  27947  ballotlemfrc  28093  cvmscld  28346  ftc1cnnc  29655  cntzsdrg  30747  limcrecl  31128  fperdvper  31205  stoweidlem57  31314  dirkercncflem3  31362  fourierdlem46  31410  lincdifsn  31975  lindslinindsimp1  32008  lincresunit3lem2  32031  lsatfixedN  33683  dochsnkr  36146  hdmaprnlem4tN  36529
  Copyright terms: Public domain W3C validator