Theorem ssdifssd 4106

Description: If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is also contained in 𝐵. Deduction form of ssdifss 4099. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
ssdifd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
ssdifssd	⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ 𝐵)

Proof of Theorem ssdifssd

Step	Hyp	Ref	Expression
1		ssdifd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		ssdifss 4099	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ 𝐵)

Syntax hints:   → wi 4   ∖ cdif 3908   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-ss 3928

This theorem is referenced by:  xpord3pred  8108  unblem1  9215  fin23lem26  10254  fin23lem29  10270  isf32lem8  10289  fprodfvdvdsd  16280  mrieqvlemd  17570  mrieqv2d  17580  mrissmrid  17582  mreexmrid  17584  mreexexlem2d  17586  mreexexlem4d  17588  acsfiindd  18494  ablfac1eulem  19988  c0rnghm  20455  cntzsdrg  20722  lbspss  21021  lspsolv  21085  lsppratlem3  21091  lsppratlem4  21092  lspprat  21095  islbs2  21096  islbs3  21097  lbsextlem2  21101  lbsextlem3  21102  lbsextlem4  21103  lpss3  23064  islp3  23066  neitr  23100  restlp  23103  lpcls  23284  qtoprest  23637  ufinffr  23849  cldsubg  24031  xrge0gsumle  24755  bcthlem5  25261  rrxmval  25338  cmmbl  25468  nulmbl2  25470  shftmbl  25472  iundisj2  25483  uniiccdif  25512  uniiccmbl  25524  itg1val2  25618  itg1cl  25619  itg1ge0  25620  i1fadd  25629  itg1addlem5  25634  i1fmulc  25637  itg1mulc  25638  itg10a  25644  itg1ge0a  25645  itg1climres  25648  mbfi1fseqlem4  25652  itgss3  25749  limcdif  25810  limcnlp  25812  limcmpt2  25818  perfdvf  25837  dvcnp2  25854  dvcnp2OLD  25855  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  dvferm1  25922  dvferm2  25924  ftc1lem6  25981  ig1peu  26113  ig1pdvds  26118  taylthlem1  26314  taylthlem2  26315  taylthlem2OLD  26316  ulmdvlem3  26344  rlimcnp  26908  wilthlem2  27012  newf  27803  elpwdifcl  32505  iundisj2f  32569  ofpreima2  32640  iundisj2fi  32770  tocyccntz  33116  elrgspnsubrunlem1  33214  elrgspnsubrunlem2  33215  0nellinds  33334  elrspunidl  33392  rprmdvdsprod  33498  ig1pmindeg  33560  lindsunlem  33613  lbsdiflsp0  33615  dimlssid  33621  fldextrspunlsp  33662  omsmeas  34307  eulerpartlemgs2  34364  ballotlemfrc  34511  hgt750lemd  34632  hgt750leme  34642  cvmscld  35253  unbdqndv1  36489  lindsadd  37600  lindsenlbs  37602  ftc1cnnc  37679  lsatfixedN  38995  dochsnkr  41459  hdmaprnlem4tN  41839  redvmptabs  42341  prjcrv0  42614  supminfxr2  45458  limcrecl  45620  cnrefiisplem  45820  fperdvper  45910  ismbl3  45977  ovolsplit  45979  ismbl4  45984  stoweidlem57  46048  dirkercncflem3  46096  fourierdlem42  46140  fourierdlem46  46143  fourierdlem62  46159  caragenuncllem  46503  caragendifcl  46505  omelesplit  46509  carageniuncllem2  46513  carageniuncl  46514  caragenel2d  46523  hspmbllem3  46619  hspmbl  46620  ovnsplit  46639  vonvolmbllem  46651  vonvolmbl  46652  lincdifsn  48406  lindslinindsimp1  48439  lincresunit3lem2  48462