Theorem ssdifssd 4087

Description: If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is also contained in 𝐵. Deduction form of ssdifss 4080. (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 4080	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ 𝐵)

Syntax hints:   → wi 4   ∖ cdif 3886   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-ss 3906

This theorem is referenced by:  xpord3pred  8102  unblem1  9202  fin23lem26  10247  fin23lem29  10263  isf32lem8  10282  fprodfvdvdsd  16303  mrieqvlemd  17595  mrieqv2d  17605  mrissmrid  17607  mreexmrid  17609  mreexexlem2d  17611  mreexexlem4d  17613  acsfiindd  18519  ablfac1eulem  20049  c0rnghm  20512  cntzsdrg  20779  lbspss  21077  lspsolv  21141  lsppratlem3  21147  lsppratlem4  21148  lspprat  21151  islbs2  21152  islbs3  21153  lbsextlem2  21157  lbsextlem3  21158  lbsextlem4  21159  lpss3  23109  islp3  23111  neitr  23145  restlp  23148  lpcls  23329  qtoprest  23682  ufinffr  23894  cldsubg  24076  xrge0gsumle  24799  bcthlem5  25295  rrxmval  25372  cmmbl  25501  nulmbl2  25503  shftmbl  25505  iundisj2  25516  uniiccdif  25545  uniiccmbl  25557  itg1val2  25651  itg1cl  25652  itg1ge0  25653  i1fadd  25662  itg1addlem5  25667  i1fmulc  25670  itg1mulc  25671  itg10a  25677  itg1ge0a  25678  itg1climres  25681  mbfi1fseqlem4  25685  itgss3  25782  limcdif  25843  limcnlp  25845  limcmpt2  25851  perfdvf  25870  dvcnp2  25887  dvaddbr  25905  dvmulbr  25906  dvferm1  25952  dvferm2  25954  ftc1lem6  26008  ig1peu  26140  ig1pdvds  26145  taylthlem1  26338  taylthlem2  26339  ulmdvlem3  26367  rlimcnp  26929  wilthlem2  27032  newf  27830  elpwdifcl  32596  iundisj2f  32660  ofpreima2  32739  iundisj2fi  32870  tocyccntz  33205  fxpsdrg  33236  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  0nellinds  33430  elrspunidl  33488  rprmdvdsprod  33594  ig1pmindeg  33662  lindsunlem  33768  lbsdiflsp0  33770  dimlssid  33776  fldextrspunlsp  33818  omsmeas  34467  eulerpartlemgs2  34524  ballotlemfrc  34671  hgt750lemd  34792  hgt750leme  34802  cvmscld  35455  unbdqndv1  36768  lindsadd  37934  lindsenlbs  37936  ftc1cnnc  38013  lsatfixedN  39455  dochsnkr  41918  hdmaprnlem4tN  42298  redvmptabs  42792  prjcrv0  43066  supminfxr2  45897  limcrecl  46059  cnrefiisplem  46257  fperdvper  46347  ismbl3  46414  ovolsplit  46416  ismbl4  46421  stoweidlem57  46485  dirkercncflem3  46533  fourierdlem42  46577  fourierdlem46  46580  fourierdlem62  46596  caragenuncllem  46940  caragendifcl  46942  omelesplit  46946  carageniuncllem2  46950  carageniuncl  46951  caragenel2d  46960  hspmbllem3  47056  hspmbl  47057  ovnsplit  47076  vonvolmbllem  47088  vonvolmbl  47089  lincdifsn  48900  lindslinindsimp1  48933  lincresunit3lem2  48956