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

Theorem ssdifssd 3482
Description: If  A is contained in  B, then  ( A  \  C ) is also contained in  B. Deduction form of ssdifss 3475. (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 3475 . 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 3313    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-dif 3319  df-in 3323  df-ss 3330
This theorem is referenced by:  unblem1  7552  fin23lem26  8482  fin23lem29  8498  isf32lem8  8517  mrieqvlemd  14549  mrieqv2d  14559  mrissmrid  14561  mreexmrid  14563  mreexexlem2d  14565  mreexexlem4d  14567  acsfiindd  15329  ablfac1eulem  16546  lbspss  17084  lspsolv  17145  lsppratlem3  17151  lsppratlem4  17152  lspprat  17155  islbs2  17156  islbs3  17157  lbsextlem2  17161  lbsextlem3  17162  lbsextlem4  17163  lpss3  18589  neitr  18625  restlp  18628  lpcls  18809  qtoprest  19131  ufinffr  19343  cldsubg  19522  xrge0gsumle  20251  bcthlem5  20680  rrxmval  20745  cmmbl  20857  nulmbl2  20859  shftmbl  20861  iundisj2  20871  uniiccdif  20899  uniiccmbl  20911  itg1val2  21003  itg1cl  21004  itg1ge0  21005  i1fadd  21014  itg1addlem5  21019  i1fmulc  21022  itg1mulc  21023  itg10a  21029  itg1ge0a  21030  itg1climres  21033  mbfi1fseqlem4  21037  itgss3  21133  limcdif  21192  limcnlp  21194  limcmpt2  21200  perfdvf  21219  dvcnp2  21235  dvaddbr  21253  dvmulbr  21254  dvferm1  21298  dvferm2  21300  ftc1lem6  21354  ig1peu  21527  ig1pdvds  21532  taylthlem1  21722  taylthlem2  21723  ulmdvlem3  21751  rlimcnp  22243  wilthlem2  22291  iundisj2f  25755  iundisj2fi  25903  eulerpartlemgs2  26610  ballotlemfrc  26756  cvmscld  27009  ftc1cnnc  28307  cntzsdrg  29401  stoweidlem57  29695  lincdifsn  30664  lindslinindsimp1  30697  lincresunit3lem2  30720  lsatfixedN  32224  dochsnkr  34687  hdmaprnlem4tN  35070
  Copyright terms: Public domain W3C validator