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

Theorem ssdifssd 3477
Description: If  A is contained in  B, then  ( A  \  C ) is also contained in  B. Deduction form of ssdifss 3470. (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 3470 . 2  |-  ( A 
C_  B  ->  ( A  \  C )  C_  B )
31, 2syl 16 1  |-  ( ph  ->  ( A  \  C
)  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \ cdif 3309    C_ wss 3312
This theorem is referenced by:  unblem1  7351  fin23lem26  8195  fin23lem29  8211  isf32lem8  8230  mrieqvlemd  13844  mrieqv2d  13854  mrissmrid  13856  mreexmrid  13858  mreexexlem2d  13860  mreexexlem4d  13862  acsfiindd  14593  ablfac1eulem  15620  lbspss  16144  lspsolv  16205  lsppratlem3  16211  lsppratlem4  16212  lspprat  16215  islbs2  16216  islbs3  16217  lbsextlem2  16221  lbsextlem3  16222  lbsextlem4  16223  lpss3  17198  neitr  17234  restlp  17237  lpcls  17418  qtoprest  17739  ufinffr  17951  cldsubg  18130  xrge0gsumle  18854  bcthlem5  19271  cmmbl  19419  nulmbl2  19421  shftmbl  19423  iundisj2  19433  uniiccdif  19460  uniiccmbl  19472  itg1val2  19566  itg1cl  19567  itg1ge0  19568  i1fadd  19577  itg1addlem5  19582  i1fmulc  19585  itg1mulc  19586  itg10a  19592  itg1ge0a  19593  itg1climres  19596  mbfi1fseqlem4  19600  itgss3  19696  limcdif  19753  limcnlp  19755  limcmpt2  19761  perfdvf  19780  dvcnp2  19796  dvaddbr  19814  dvmulbr  19815  dvferm1  19859  dvferm2  19861  ftc1lem6  19915  ig1peu  20084  ig1pdvds  20089  taylthlem1  20279  taylthlem2  20280  ulmdvlem3  20308  rlimcnp  20794  wilthlem2  20842  iundisj2f  24020  iundisj2fi  24143  ballotlemfrc  24774  cvmscld  24950  ftc1cnnc  26242  cntzsdrg  27442  stoweidlem57  27737  lsatfixedN  29708  dochsnkr  32171  hdmaprnlem4tN  32554
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-dif 3315  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator