Theorem ssdifssd 4098

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906  df-ss 3920

This theorem is referenced by:  xpord3pred  8085  unblem1  9181  fin23lem26  10219  fin23lem29  10235  isf32lem8  10254  fprodfvdvdsd  16245  mrieqvlemd  17535  mrieqv2d  17545  mrissmrid  17547  mreexmrid  17549  mreexexlem2d  17551  mreexexlem4d  17553  acsfiindd  18459  ablfac1eulem  19953  c0rnghm  20420  cntzsdrg  20687  lbspss  20986  lspsolv  21050  lsppratlem3  21056  lsppratlem4  21057  lspprat  21060  islbs2  21061  islbs3  21062  lbsextlem2  21066  lbsextlem3  21067  lbsextlem4  21068  lpss3  23029  islp3  23031  neitr  23065  restlp  23068  lpcls  23249  qtoprest  23602  ufinffr  23814  cldsubg  23996  xrge0gsumle  24720  bcthlem5  25226  rrxmval  25303  cmmbl  25433  nulmbl2  25435  shftmbl  25437  iundisj2  25448  uniiccdif  25477  uniiccmbl  25489  itg1val2  25583  itg1cl  25584  itg1ge0  25585  i1fadd  25594  itg1addlem5  25599  i1fmulc  25602  itg1mulc  25603  itg10a  25609  itg1ge0a  25610  itg1climres  25613  mbfi1fseqlem4  25617  itgss3  25714  limcdif  25775  limcnlp  25777  limcmpt2  25783  perfdvf  25802  dvcnp2  25819  dvcnp2OLD  25820  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  dvferm1  25887  dvferm2  25889  ftc1lem6  25946  ig1peu  26078  ig1pdvds  26083  taylthlem1  26279  taylthlem2  26280  taylthlem2OLD  26281  ulmdvlem3  26309  rlimcnp  26873  wilthlem2  26977  newf  27768  elpwdifcl  32470  iundisj2f  32534  ofpreima2  32610  iundisj2fi  32741  tocyccntz  33087  fxpsdrg  33118  elrgspnsubrunlem1  33188  elrgspnsubrunlem2  33189  0nellinds  33308  elrspunidl  33366  rprmdvdsprod  33472  ig1pmindeg  33535  lindsunlem  33597  lbsdiflsp0  33599  dimlssid  33605  fldextrspunlsp  33647  omsmeas  34297  eulerpartlemgs2  34354  ballotlemfrc  34501  hgt750lemd  34622  hgt750leme  34632  cvmscld  35256  unbdqndv1  36492  lindsadd  37603  lindsenlbs  37605  ftc1cnnc  37682  lsatfixedN  38998  dochsnkr  41461  hdmaprnlem4tN  41841  redvmptabs  42343  prjcrv0  42616  supminfxr2  45458  limcrecl  45620  cnrefiisplem  45820  fperdvper  45910  ismbl3  45977  ovolsplit  45979  ismbl4  45984  stoweidlem57  46048  dirkercncflem3  46096  fourierdlem42  46140  fourierdlem46  46143  fourierdlem62  46159  caragenuncllem  46503  caragendifcl  46505  omelesplit  46509  carageniuncllem2  46513  carageniuncl  46514  caragenel2d  46523  hspmbllem3  46619  hspmbl  46620  ovnsplit  46639  vonvolmbllem  46651  vonvolmbl  46652  lincdifsn  48419  lindslinindsimp1  48452  lincresunit3lem2  48475