Theorem ssdifssd 4097

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

Syntax hints:   → wi 4   ∖ cdif 3896   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902  df-ss 3916

This theorem is referenced by:  xpord3pred  8092  unblem1  9190  fin23lem26  10233  fin23lem29  10249  isf32lem8  10268  fprodfvdvdsd  16259  mrieqvlemd  17550  mrieqv2d  17560  mrissmrid  17562  mreexmrid  17564  mreexexlem2d  17566  mreexexlem4d  17568  acsfiindd  18474  ablfac1eulem  20001  c0rnghm  20466  cntzsdrg  20733  lbspss  21032  lspsolv  21096  lsppratlem3  21102  lsppratlem4  21103  lspprat  21106  islbs2  21107  islbs3  21108  lbsextlem2  21112  lbsextlem3  21113  lbsextlem4  21114  lpss3  23086  islp3  23088  neitr  23122  restlp  23125  lpcls  23306  qtoprest  23659  ufinffr  23871  cldsubg  24053  xrge0gsumle  24776  bcthlem5  25282  rrxmval  25359  cmmbl  25489  nulmbl2  25491  shftmbl  25493  iundisj2  25504  uniiccdif  25533  uniiccmbl  25545  itg1val2  25639  itg1cl  25640  itg1ge0  25641  i1fadd  25650  itg1addlem5  25655  i1fmulc  25658  itg1mulc  25659  itg10a  25665  itg1ge0a  25666  itg1climres  25669  mbfi1fseqlem4  25673  itgss3  25770  limcdif  25831  limcnlp  25833  limcmpt2  25839  perfdvf  25858  dvcnp2  25875  dvcnp2OLD  25876  dvaddbr  25894  dvmulbr  25895  dvmulbrOLD  25896  dvferm1  25943  dvferm2  25945  ftc1lem6  26002  ig1peu  26134  ig1pdvds  26139  taylthlem1  26335  taylthlem2  26336  taylthlem2OLD  26337  ulmdvlem3  26365  rlimcnp  26929  wilthlem2  27033  newf  27826  elpwdifcl  32550  iundisj2f  32614  ofpreima2  32693  iundisj2fi  32826  tocyccntz  33175  fxpsdrg  33206  elrgspnsubrunlem1  33278  elrgspnsubrunlem2  33279  0nellinds  33400  elrspunidl  33458  rprmdvdsprod  33564  ig1pmindeg  33632  lindsunlem  33730  lbsdiflsp0  33732  dimlssid  33738  fldextrspunlsp  33780  omsmeas  34429  eulerpartlemgs2  34486  ballotlemfrc  34633  hgt750lemd  34754  hgt750leme  34764  cvmscld  35416  unbdqndv1  36651  lindsadd  37753  lindsenlbs  37755  ftc1cnnc  37832  lsatfixedN  39208  dochsnkr  41671  hdmaprnlem4tN  42051  redvmptabs  42557  prjcrv0  42818  supminfxr2  45655  limcrecl  45817  cnrefiisplem  46015  fperdvper  46105  ismbl3  46172  ovolsplit  46174  ismbl4  46179  stoweidlem57  46243  dirkercncflem3  46291  fourierdlem42  46335  fourierdlem46  46338  fourierdlem62  46354  caragenuncllem  46698  caragendifcl  46700  omelesplit  46704  carageniuncllem2  46708  carageniuncl  46709  caragenel2d  46718  hspmbllem3  46814  hspmbl  46815  ovnsplit  46834  vonvolmbllem  46846  vonvolmbl  46847  lincdifsn  48612  lindslinindsimp1  48645  lincresunit3lem2  48668