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

Theorem ssdifssd 3429
Description: If  A is contained in  B, then  ( A  \  C ) is also contained in  B. Deduction form of ssdifss 3422. (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 3422 . 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 3261    C_ wss 3264
This theorem is referenced by:  unblem1  7296  fin23lem26  8139  fin23lem29  8155  isf32lem8  8174  mrieqvlemd  13782  mrieqv2d  13792  mrissmrid  13794  mreexmrid  13796  mreexexlem2d  13798  mreexexlem4d  13800  acsfiindd  14531  ablfac1eulem  15558  lbspss  16082  lspsolv  16143  lsppratlem3  16149  lsppratlem4  16150  lspprat  16153  islbs2  16154  islbs3  16155  lbsextlem2  16159  lbsextlem3  16160  lbsextlem4  16161  lpss3  17132  neitr  17167  restlp  17170  lpcls  17351  qtoprest  17671  ufinffr  17883  cldsubg  18062  xrge0gsumle  18736  bcthlem5  19151  cmmbl  19297  nulmbl2  19299  shftmbl  19301  iundisj2  19311  uniiccdif  19338  uniiccmbl  19350  itg1val2  19444  itg1cl  19445  itg1ge0  19446  i1fadd  19455  itg1addlem5  19460  i1fmulc  19463  itg1mulc  19464  itg10a  19470  itg1ge0a  19471  itg1climres  19474  mbfi1fseqlem4  19478  itgss3  19574  limcdif  19631  limcnlp  19633  limcmpt2  19639  perfdvf  19658  dvcnp2  19674  dvaddbr  19692  dvmulbr  19693  dvferm1  19737  dvferm2  19739  ftc1lem6  19793  ig1peu  19962  ig1pdvds  19967  taylthlem1  20157  taylthlem2  20158  ulmdvlem3  20186  rlimcnp  20672  wilthlem2  20720  iundisj2f  23874  iundisj2fi  23992  ballotlemfrc  24564  cvmscld  24740  ftc1cnnc  25980  cntzsdrg  27180  stoweidlem57  27475  lsatfixedN  29125  dochsnkr  31588  hdmaprnlem4tN  31971
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-dif 3267  df-in 3271  df-ss 3278
  Copyright terms: Public domain W3C validator