Theorem ssdifssd 4170

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

Syntax hints:   → wi 4   ∖ cdif 3973   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-ss 3993

This theorem is referenced by:  xpord3pred  8193  unblem1  9356  fin23lem26  10394  fin23lem29  10410  isf32lem8  10429  fprodfvdvdsd  16382  mrieqvlemd  17687  mrieqv2d  17697  mrissmrid  17699  mreexmrid  17701  mreexexlem2d  17703  mreexexlem4d  17705  acsfiindd  18623  ablfac1eulem  20116  c0rnghm  20561  cntzsdrg  20825  lbspss  21104  lspsolv  21168  lsppratlem3  21174  lsppratlem4  21175  lspprat  21178  islbs2  21179  islbs3  21180  lbsextlem2  21184  lbsextlem3  21185  lbsextlem4  21186  lpss3  23173  islp3  23175  neitr  23209  restlp  23212  lpcls  23393  qtoprest  23746  ufinffr  23958  cldsubg  24140  xrge0gsumle  24874  bcthlem5  25381  rrxmval  25458  cmmbl  25588  nulmbl2  25590  shftmbl  25592  iundisj2  25603  uniiccdif  25632  uniiccmbl  25644  itg1val2  25738  itg1cl  25739  itg1ge0  25740  i1fadd  25749  itg1addlem5  25755  i1fmulc  25758  itg1mulc  25759  itg10a  25765  itg1ge0a  25766  itg1climres  25769  mbfi1fseqlem4  25773  itgss3  25870  limcdif  25931  limcnlp  25933  limcmpt2  25939  perfdvf  25958  dvcnp2  25975  dvcnp2OLD  25976  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvferm1  26043  dvferm2  26045  ftc1lem6  26102  ig1peu  26234  ig1pdvds  26239  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmdvlem3  26463  rlimcnp  27026  wilthlem2  27130  newf  27915  elpwdifcl  32556  iundisj2f  32612  ofpreima2  32684  iundisj2fi  32802  tocyccntz  33137  0nellinds  33363  elrspunidl  33421  rprmdvdsprod  33527  ig1pmindeg  33587  lindsunlem  33637  lbsdiflsp0  33639  dimlssid  33645  omsmeas  34288  eulerpartlemgs2  34345  ballotlemfrc  34491  hgt750lemd  34625  hgt750leme  34635  cvmscld  35241  unbdqndv1  36474  lindsadd  37573  lindsenlbs  37575  ftc1cnnc  37652  lsatfixedN  38965  dochsnkr  41429  hdmaprnlem4tN  41809  prjcrv0  42588  supminfxr2  45384  limcrecl  45550  cnrefiisplem  45750  fperdvper  45840  ismbl3  45907  ovolsplit  45909  ismbl4  45914  stoweidlem57  45978  dirkercncflem3  46026  fourierdlem42  46070  fourierdlem46  46073  fourierdlem62  46089  caragenuncllem  46433  caragendifcl  46435  omelesplit  46439  carageniuncllem2  46443  carageniuncl  46444  caragenel2d  46453  hspmbllem3  46549  hspmbl  46550  ovnsplit  46569  vonvolmbllem  46581  vonvolmbl  46582  lincdifsn  48153  lindslinindsimp1  48186  lincresunit3lem2  48209