Theorem ssdifssd 4079

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

Syntax hints:   → wi 4   ∖ cdif 3881   ⊆ wss 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-dif 3887  df-ss 3901

This theorem is referenced by:  xpord3pred  8094  unblem1  9196  fin23lem26  10243  fin23lem29  10259  isf32lem8  10278  fprodfvdvdsd  16298  mrieqvlemd  17590  mrieqv2d  17600  mrissmrid  17602  mreexmrid  17604  mreexexlem2d  17606  mreexexlem4d  17608  acsfiindd  18514  ablfac1eulem  20043  c0rnghm  20510  cntzsdrg  20777  lbspss  21075  lspsolv  21139  lsppratlem3  21145  lsppratlem4  21146  lspprat  21149  islbs2  21150  islbs3  21151  lbsextlem2  21155  lbsextlem3  21156  lbsextlem4  21157  lpss3  23130  islp3  23132  neitr  23166  restlp  23169  lpcls  23350  qtoprest  23703  ufinffr  23915  cldsubg  24097  xrge0gsumle  24820  bcthlem5  25316  rrxmval  25393  cmmbl  25522  nulmbl2  25524  shftmbl  25526  iundisj2  25537  uniiccdif  25566  uniiccmbl  25578  itg1val2  25672  itg1cl  25673  itg1ge0  25674  i1fadd  25683  itg1addlem5  25688  i1fmulc  25691  itg1mulc  25692  itg10a  25698  itg1ge0a  25699  itg1climres  25702  mbfi1fseqlem4  25706  itgss3  25803  limcdif  25864  limcnlp  25866  limcmpt2  25872  perfdvf  25891  dvcnp2  25908  dvaddbr  25926  dvmulbr  25927  dvferm1  25973  dvferm2  25975  ftc1lem6  26029  ig1peu  26161  ig1pdvds  26166  taylthlem1  26359  taylthlem2  26360  ulmdvlem3  26388  rlimcnp  26950  wilthlem2  27053  newf  27850  elpwdifcl  32616  iundisj2f  32681  ofpreima2  32760  iundisj2fi  32891  tocyccntz  33227  fxpsdrg  33258  elrgspnsubrunlem1  33330  elrgspnsubrunlem2  33331  0nellinds  33455  elrspunidl  33513  rprmdvdsprod  33627  ig1pmindeg  33695  lindsunlem  33818  lbsdiflsp0  33820  dimlssid  33826  fldextrspunlsp  33868  omsmeas  34517  eulerpartlemgs2  34574  ballotlemfrc  34721  hgt750lemd  34842  hgt750leme  34852  cvmscld  35514  unbdqndv1  36827  lindsadd  37993  lindsenlbs  37995  ftc1cnnc  38072  lsatfixedN  39514  dochsnkr  41977  hdmaprnlem4tN  42357  redvmptabs  42850  prjcrv0  43096  supminfxr2  45924  limcrecl  46086  cnrefiisplem  46284  fperdvper  46374  ismbl3  46441  ovolsplit  46443  ismbl4  46448  stoweidlem57  46512  dirkercncflem3  46560  fourierdlem42  46604  fourierdlem46  46607  fourierdlem62  46623  caragenuncllem  46967  caragendifcl  46969  omelesplit  46973  carageniuncllem2  46977  carageniuncl  46978  caragenel2d  46987  hspmbllem3  47083  hspmbl  47084  ovnsplit  47103  vonvolmbllem  47115  vonvolmbl  47116  lincdifsn  48927  lindslinindsimp1  48960  lincresunit3lem2  48983