Theorem ssdifssd 4100

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-dif 3905  df-ss 3919

This theorem is referenced by:  xpord3pred  8096  unblem1  9196  fin23lem26  10239  fin23lem29  10255  isf32lem8  10274  fprodfvdvdsd  16265  mrieqvlemd  17556  mrieqv2d  17566  mrissmrid  17568  mreexmrid  17570  mreexexlem2d  17572  mreexexlem4d  17574  acsfiindd  18480  ablfac1eulem  20007  c0rnghm  20472  cntzsdrg  20739  lbspss  21038  lspsolv  21102  lsppratlem3  21108  lsppratlem4  21109  lspprat  21112  islbs2  21113  islbs3  21114  lbsextlem2  21118  lbsextlem3  21119  lbsextlem4  21120  lpss3  23092  islp3  23094  neitr  23128  restlp  23131  lpcls  23312  qtoprest  23665  ufinffr  23877  cldsubg  24059  xrge0gsumle  24782  bcthlem5  25288  rrxmval  25365  cmmbl  25495  nulmbl2  25497  shftmbl  25499  iundisj2  25510  uniiccdif  25539  uniiccmbl  25551  itg1val2  25645  itg1cl  25646  itg1ge0  25647  i1fadd  25656  itg1addlem5  25661  i1fmulc  25664  itg1mulc  25665  itg10a  25671  itg1ge0a  25672  itg1climres  25675  mbfi1fseqlem4  25679  itgss3  25776  limcdif  25837  limcnlp  25839  limcmpt2  25845  perfdvf  25864  dvcnp2  25881  dvcnp2OLD  25882  dvaddbr  25900  dvmulbr  25901  dvmulbrOLD  25902  dvferm1  25949  dvferm2  25951  ftc1lem6  26008  ig1peu  26140  ig1pdvds  26145  taylthlem1  26341  taylthlem2  26342  taylthlem2OLD  26343  ulmdvlem3  26371  rlimcnp  26935  wilthlem2  27039  newf  27838  elpwdifcl  32604  iundisj2f  32668  ofpreima2  32747  iundisj2fi  32879  tocyccntz  33228  fxpsdrg  33259  elrgspnsubrunlem1  33331  elrgspnsubrunlem2  33332  0nellinds  33453  elrspunidl  33511  rprmdvdsprod  33617  ig1pmindeg  33685  lindsunlem  33783  lbsdiflsp0  33785  dimlssid  33791  fldextrspunlsp  33833  omsmeas  34482  eulerpartlemgs2  34539  ballotlemfrc  34686  hgt750lemd  34807  hgt750leme  34817  cvmscld  35469  unbdqndv1  36710  lindsadd  37816  lindsenlbs  37818  ftc1cnnc  37895  lsatfixedN  39337  dochsnkr  41800  hdmaprnlem4tN  42180  redvmptabs  42682  prjcrv0  42943  supminfxr2  45780  limcrecl  45942  cnrefiisplem  46140  fperdvper  46230  ismbl3  46297  ovolsplit  46299  ismbl4  46304  stoweidlem57  46368  dirkercncflem3  46416  fourierdlem42  46460  fourierdlem46  46463  fourierdlem62  46479  caragenuncllem  46823  caragendifcl  46825  omelesplit  46829  carageniuncllem2  46833  carageniuncl  46834  caragenel2d  46843  hspmbllem3  46939  hspmbl  46940  ovnsplit  46959  vonvolmbllem  46971  vonvolmbl  46972  lincdifsn  48737  lindslinindsimp1  48770  lincresunit3lem2  48793