Theorem ssdifssd 4143

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

Syntax hints:   → wi 4   ∖ cdif 3946   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966

This theorem is referenced by:  xpord3pred  8138  unblem1  9295  fin23lem26  10320  fin23lem29  10336  isf32lem8  10355  fprodfvdvdsd  16277  mrieqvlemd  17573  mrieqv2d  17583  mrissmrid  17585  mreexmrid  17587  mreexexlem2d  17589  mreexexlem4d  17591  acsfiindd  18506  ablfac1eulem  19942  cntzsdrg  20418  lbspss  20693  lspsolv  20756  lsppratlem3  20762  lsppratlem4  20763  lspprat  20766  islbs2  20767  islbs3  20768  lbsextlem2  20772  lbsextlem3  20773  lbsextlem4  20774  lpss3  22648  islp3  22650  neitr  22684  restlp  22687  lpcls  22868  qtoprest  23221  ufinffr  23433  cldsubg  23615  xrge0gsumle  24349  bcthlem5  24845  rrxmval  24922  cmmbl  25051  nulmbl2  25053  shftmbl  25055  iundisj2  25066  uniiccdif  25095  uniiccmbl  25107  itg1val2  25201  itg1cl  25202  itg1ge0  25203  i1fadd  25212  itg1addlem5  25218  i1fmulc  25221  itg1mulc  25222  itg10a  25228  itg1ge0a  25229  itg1climres  25232  mbfi1fseqlem4  25236  itgss3  25332  limcdif  25393  limcnlp  25395  limcmpt2  25401  perfdvf  25420  dvcnp2  25437  dvaddbr  25455  dvmulbr  25456  dvferm1  25502  dvferm2  25504  ftc1lem6  25558  ig1peu  25689  ig1pdvds  25694  taylthlem1  25885  taylthlem2  25886  ulmdvlem3  25914  rlimcnp  26470  wilthlem2  26573  newf  27353  elpwdifcl  31764  iundisj2f  31821  ofpreima2  31891  iundisj2fi  32008  tocyccntz  32303  0nellinds  32483  elrspunidl  32546  ig1pmindeg  32671  lindsunlem  32709  lbsdiflsp0  32711  omsmeas  33322  eulerpartlemgs2  33379  ballotlemfrc  33525  hgt750lemd  33660  hgt750leme  33670  cvmscld  34264  gg-dvcnp2  35174  gg-dvmulbr  35175  unbdqndv1  35384  lindsadd  36481  lindsenlbs  36483  ftc1cnnc  36560  lsatfixedN  37879  dochsnkr  40343  hdmaprnlem4tN  40723  prjcrv0  41375  supminfxr2  44179  limcrecl  44345  cnrefiisplem  44545  fperdvper  44635  ismbl3  44702  ovolsplit  44704  ismbl4  44709  stoweidlem57  44773  dirkercncflem3  44821  fourierdlem42  44865  fourierdlem46  44868  fourierdlem62  44884  caragenuncllem  45228  caragendifcl  45230  omelesplit  45234  carageniuncllem2  45238  carageniuncl  45239  caragenel2d  45248  hspmbllem3  45344  hspmbl  45345  ovnsplit  45364  vonvolmbllem  45376  vonvolmbl  45377  c0rnghm  46712  lincdifsn  47105  lindslinindsimp1  47138  lincresunit3lem2  47161