Theorem ssdifssd 4094

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

Syntax hints:   → wi 4   ∖ cdif 3894   ⊆ wss 3897

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-ss 3914

This theorem is referenced by:  xpord3pred  8082  unblem1  9176  fin23lem26  10216  fin23lem29  10232  isf32lem8  10251  fprodfvdvdsd  16245  mrieqvlemd  17535  mrieqv2d  17545  mrissmrid  17547  mreexmrid  17549  mreexexlem2d  17551  mreexexlem4d  17553  acsfiindd  18459  ablfac1eulem  19986  c0rnghm  20450  cntzsdrg  20717  lbspss  21016  lspsolv  21080  lsppratlem3  21086  lsppratlem4  21087  lspprat  21090  islbs2  21091  islbs3  21092  lbsextlem2  21096  lbsextlem3  21097  lbsextlem4  21098  lpss3  23059  islp3  23061  neitr  23095  restlp  23098  lpcls  23279  qtoprest  23632  ufinffr  23844  cldsubg  24026  xrge0gsumle  24749  bcthlem5  25255  rrxmval  25332  cmmbl  25462  nulmbl2  25464  shftmbl  25466  iundisj2  25477  uniiccdif  25506  uniiccmbl  25518  itg1val2  25612  itg1cl  25613  itg1ge0  25614  i1fadd  25623  itg1addlem5  25628  i1fmulc  25631  itg1mulc  25632  itg10a  25638  itg1ge0a  25639  itg1climres  25642  mbfi1fseqlem4  25646  itgss3  25743  limcdif  25804  limcnlp  25806  limcmpt2  25812  perfdvf  25831  dvcnp2  25848  dvcnp2OLD  25849  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvferm1  25916  dvferm2  25918  ftc1lem6  25975  ig1peu  26107  ig1pdvds  26112  taylthlem1  26308  taylthlem2  26309  taylthlem2OLD  26310  ulmdvlem3  26338  rlimcnp  26902  wilthlem2  27006  newf  27799  elpwdifcl  32506  iundisj2f  32570  ofpreima2  32648  iundisj2fi  32779  tocyccntz  33113  fxpsdrg  33144  elrgspnsubrunlem1  33214  elrgspnsubrunlem2  33215  0nellinds  33335  elrspunidl  33393  rprmdvdsprod  33499  ig1pmindeg  33562  lindsunlem  33637  lbsdiflsp0  33639  dimlssid  33645  fldextrspunlsp  33687  omsmeas  34336  eulerpartlemgs2  34393  ballotlemfrc  34540  hgt750lemd  34661  hgt750leme  34671  cvmscld  35317  unbdqndv1  36552  lindsadd  37652  lindsenlbs  37654  ftc1cnnc  37731  lsatfixedN  39107  dochsnkr  41570  hdmaprnlem4tN  41950  redvmptabs  42452  prjcrv0  42725  supminfxr2  45566  limcrecl  45728  cnrefiisplem  45926  fperdvper  46016  ismbl3  46083  ovolsplit  46085  ismbl4  46090  stoweidlem57  46154  dirkercncflem3  46202  fourierdlem42  46246  fourierdlem46  46249  fourierdlem62  46265  caragenuncllem  46609  caragendifcl  46611  omelesplit  46615  carageniuncllem2  46619  carageniuncl  46620  caragenel2d  46629  hspmbllem3  46725  hspmbl  46726  ovnsplit  46745  vonvolmbllem  46757  vonvolmbl  46758  lincdifsn  48524  lindslinindsimp1  48557  lincresunit3lem2  48580