Theorem ssdifssd 4102

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

Syntax hints:   → wi 4   ∖ cdif 3903   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-dif 3909  df-ss 3923

This theorem is referenced by:  xpord3pred  8134  unblem1  9238  fin23lem26  10284  fin23lem29  10300  isf32lem8  10319  fprodfvdvdsd  16370  mrieqvlemd  17663  mrieqv2d  17673  mrissmrid  17675  mreexmrid  17677  mreexexlem2d  17679  mreexexlem4d  17681  acsfiindd  18587  ablfac1eulem  20116  c0rnghm  20587  cntzsdrg  20853  lbspss  21151  lspsolv  21215  lsppratlem3  21221  lsppratlem4  21222  lspprat  21225  islbs2  21226  islbs3  21227  lbsextlem2  21231  lbsextlem3  21232  lbsextlem4  21233  lpss3  23206  islp3  23208  neitr  23242  restlp  23245  lpcls  23426  qtoprest  23779  ufinffr  23991  cldsubg  24173  xrge0gsumle  24896  bcthlem5  25392  rrxmval  25469  cmmbl  25598  nulmbl2  25600  shftmbl  25602  iundisj2  25613  uniiccdif  25642  uniiccmbl  25654  itg1val2  25748  itg1cl  25749  itg1ge0  25750  i1fadd  25759  itg1addlem5  25764  i1fmulc  25767  itg1mulc  25768  itg10a  25774  itg1ge0a  25775  itg1climres  25778  mbfi1fseqlem4  25782  itgss3  25879  limcdif  25940  limcnlp  25942  limcmpt2  25948  perfdvf  25967  dvcnp2  25984  dvaddbr  26002  dvmulbr  26003  dvferm1  26049  dvferm2  26051  ftc1lem6  26105  ig1peu  26237  ig1pdvds  26242  taylthlem1  26438  taylthlem2  26439  ulmdvlem3  26467  rlimcnp  27032  wilthlem2  27135  newf  27933  elpwdifcl  32727  iundisj2f  32792  ofpreima2  32870  iundisj2fi  33001  tocyccntz  33326  fxpsdrg  33357  elrgspnsubrunlem1  33430  elrgspnsubrunlem2  33431  0nellinds  33558  elrspunidl  33616  rprmdvdsprod  33732  ig1pmindeg  33800  lindsunlem  33923  lbsdiflsp0  33925  dimlssid  33931  fldextrspunlsp  33973  omsmeas  34622  eulerpartlemgs2  34679  ballotlemfrc  34826  hgt750lemd  34944  hgt750leme  34954  cvmscld  35628  unbdqndv1  36951  lindsadd  38117  lindsenlbs  38119  ftc1cnnc  38196  lsatfixedN  39638  dochsnkr  42101  hdmaprnlem4tN  42481  redvmptabs  42974  prjcrv0  43220  supminfxr2  46048  limcrecl  46210  cnrefiisplem  46408  fperdvper  46498  ismbl3  46565  ovolsplit  46567  ismbl4  46572  stoweidlem57  46636  dirkercncflem3  46684  fourierdlem42  46728  fourierdlem46  46731  fourierdlem62  46747  caragenuncllem  47091  caragendifcl  47093  omelesplit  47097  carageniuncllem2  47101  carageniuncl  47102  caragenel2d  47111  hspmbllem3  47207  hspmbl  47208  ovnsplit  47227  vonvolmbllem  47239  vonvolmbl  47240  lincdifsn  49051  lindslinindsimp1  49084  lincresunit3lem2  49107