Theorem ssdifssd 4156

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

Syntax hints:   → wi 4   ∖ cdif 3959   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-ss 3979

This theorem is referenced by:  xpord3pred  8175  unblem1  9325  fin23lem26  10362  fin23lem29  10378  isf32lem8  10397  fprodfvdvdsd  16367  mrieqvlemd  17673  mrieqv2d  17683  mrissmrid  17685  mreexmrid  17687  mreexexlem2d  17689  mreexexlem4d  17691  acsfiindd  18610  ablfac1eulem  20106  c0rnghm  20551  cntzsdrg  20819  lbspss  21098  lspsolv  21162  lsppratlem3  21168  lsppratlem4  21169  lspprat  21172  islbs2  21173  islbs3  21174  lbsextlem2  21178  lbsextlem3  21179  lbsextlem4  21180  lpss3  23167  islp3  23169  neitr  23203  restlp  23206  lpcls  23387  qtoprest  23740  ufinffr  23952  cldsubg  24134  xrge0gsumle  24868  bcthlem5  25375  rrxmval  25452  cmmbl  25582  nulmbl2  25584  shftmbl  25586  iundisj2  25597  uniiccdif  25626  uniiccmbl  25638  itg1val2  25732  itg1cl  25733  itg1ge0  25734  i1fadd  25743  itg1addlem5  25749  i1fmulc  25752  itg1mulc  25753  itg10a  25759  itg1ge0a  25760  itg1climres  25763  mbfi1fseqlem4  25767  itgss3  25864  limcdif  25925  limcnlp  25927  limcmpt2  25933  perfdvf  25952  dvcnp2  25969  dvcnp2OLD  25970  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvferm1  26037  dvferm2  26039  ftc1lem6  26096  ig1peu  26228  ig1pdvds  26233  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmdvlem3  26459  rlimcnp  27022  wilthlem2  27126  newf  27911  elpwdifcl  32553  iundisj2f  32609  ofpreima2  32682  iundisj2fi  32804  tocyccntz  33146  0nellinds  33377  elrspunidl  33435  rprmdvdsprod  33541  ig1pmindeg  33601  lindsunlem  33651  lbsdiflsp0  33653  dimlssid  33659  omsmeas  34304  eulerpartlemgs2  34361  ballotlemfrc  34507  hgt750lemd  34641  hgt750leme  34651  cvmscld  35257  unbdqndv1  36490  lindsadd  37599  lindsenlbs  37601  ftc1cnnc  37678  lsatfixedN  38990  dochsnkr  41454  hdmaprnlem4tN  41834  redvmptabs  42368  prjcrv0  42619  supminfxr2  45418  limcrecl  45584  cnrefiisplem  45784  fperdvper  45874  ismbl3  45941  ovolsplit  45943  ismbl4  45948  stoweidlem57  46012  dirkercncflem3  46060  fourierdlem42  46104  fourierdlem46  46107  fourierdlem62  46123  caragenuncllem  46467  caragendifcl  46469  omelesplit  46473  carageniuncllem2  46477  carageniuncl  46478  caragenel2d  46487  hspmbllem3  46583  hspmbl  46584  ovnsplit  46603  vonvolmbllem  46615  vonvolmbl  46616  lincdifsn  48269  lindslinindsimp1  48302  lincresunit3lem2  48325