Theorem ssdifssd 4070

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

Syntax hints:   → wi 4   ∖ cdif 3878   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898

This theorem is referenced by:  unblem1  8754  fin23lem26  9736  fin23lem29  9752  isf32lem8  9771  fprodfvdvdsd  15675  mrieqvlemd  16892  mrieqv2d  16902  mrissmrid  16904  mreexmrid  16906  mreexexlem2d  16908  mreexexlem4d  16910  acsfiindd  17779  ablfac1eulem  19187  cntzsdrg  19574  lbspss  19847  lspsolv  19908  lsppratlem3  19914  lsppratlem4  19915  lspprat  19918  islbs2  19919  islbs3  19920  lbsextlem2  19924  lbsextlem3  19925  lbsextlem4  19926  lpss3  21749  islp3  21751  neitr  21785  restlp  21788  lpcls  21969  qtoprest  22322  ufinffr  22534  cldsubg  22716  xrge0gsumle  23438  bcthlem5  23932  rrxmval  24009  cmmbl  24138  nulmbl2  24140  shftmbl  24142  iundisj2  24153  uniiccdif  24182  uniiccmbl  24194  itg1val2  24288  itg1cl  24289  itg1ge0  24290  i1fadd  24299  itg1addlem5  24304  i1fmulc  24307  itg1mulc  24308  itg10a  24314  itg1ge0a  24315  itg1climres  24318  mbfi1fseqlem4  24322  itgss3  24418  limcdif  24479  limcnlp  24481  limcmpt2  24487  perfdvf  24506  dvcnp2  24523  dvaddbr  24541  dvmulbr  24542  dvferm1  24588  dvferm2  24590  ftc1lem6  24644  ig1peu  24772  ig1pdvds  24777  taylthlem1  24968  taylthlem2  24969  ulmdvlem3  24997  rlimcnp  25551  wilthlem2  25654  elpwdifcl  30299  iundisj2f  30353  ofpreima2  30429  iundisj2fi  30546  tocyccntz  30836  0nellinds  30986  elrspunidl  31014  lindsunlem  31108  lbsdiflsp0  31110  omsmeas  31691  eulerpartlemgs2  31748  ballotlemfrc  31894  hgt750lemd  32029  hgt750leme  32039  cvmscld  32633  unbdqndv1  33960  lindsadd  35050  lindsenlbs  35052  ftc1cnnc  35129  lsatfixedN  36305  dochsnkr  38768  hdmaprnlem4tN  39148  supminfxr2  42108  limcrecl  42271  cnrefiisplem  42471  fperdvper  42561  ismbl3  42628  ovolsplit  42630  ismbl4  42635  stoweidlem57  42699  dirkercncflem3  42747  fourierdlem42  42791  fourierdlem46  42794  fourierdlem62  42810  caragenuncllem  43151  caragendifcl  43153  omelesplit  43157  carageniuncllem2  43161  carageniuncl  43162  caragenel2d  43171  hspmbllem3  43267  hspmbl  43268  ovnsplit  43287  vonvolmbllem  43299  vonvolmbl  43300  c0rnghm  44537  lincdifsn  44833  lindslinindsimp1  44866  lincresunit3lem2  44889