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

Theorem ssdifssd 3515
Description: If  A is contained in  B, then  ( A  \  C ) is also contained in  B. Deduction form of ssdifss 3508. (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 3508 . 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 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:  unblem1  7585  fin23lem26  8515  fin23lem29  8531  isf32lem8  8550  mrieqvlemd  14588  mrieqv2d  14598  mrissmrid  14600  mreexmrid  14602  mreexexlem2d  14604  mreexexlem4d  14606  acsfiindd  15368  ablfac1eulem  16595  lbspss  17185  lspsolv  17246  lsppratlem3  17252  lsppratlem4  17253  lspprat  17256  islbs2  17257  islbs3  17258  lbsextlem2  17262  lbsextlem3  17263  lbsextlem4  17264  lpss3  18770  neitr  18806  restlp  18809  lpcls  18990  qtoprest  19312  ufinffr  19524  cldsubg  19703  xrge0gsumle  20432  bcthlem5  20861  rrxmval  20926  cmmbl  21038  nulmbl2  21040  shftmbl  21042  iundisj2  21052  uniiccdif  21080  uniiccmbl  21092  itg1val2  21184  itg1cl  21185  itg1ge0  21186  i1fadd  21195  itg1addlem5  21200  i1fmulc  21203  itg1mulc  21204  itg10a  21210  itg1ge0a  21211  itg1climres  21214  mbfi1fseqlem4  21218  itgss3  21314  limcdif  21373  limcnlp  21375  limcmpt2  21381  perfdvf  21400  dvcnp2  21416  dvaddbr  21434  dvmulbr  21435  dvferm1  21479  dvferm2  21481  ftc1lem6  21535  ig1peu  21665  ig1pdvds  21670  taylthlem1  21860  taylthlem2  21861  ulmdvlem3  21889  rlimcnp  22381  wilthlem2  22429  iundisj2f  25954  iundisj2fi  26103  eulerpartlemgs2  26785  ballotlemfrc  26931  cvmscld  27184  ftc1cnnc  28492  cntzsdrg  29585  stoweidlem57  29878  lincdifsn  30955  lindslinindsimp1  30988  lincresunit3lem2  31011  lsatfixedN  32750  dochsnkr  35213  hdmaprnlem4tN  35596
  Copyright terms: Public domain W3C validator