Theorem ssdifssd 4141

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

Syntax hints:   → wi 4   ∖ cdif 3944   ⊆ wss 3947

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3950  df-in 3954  df-ss 3964

This theorem is referenced by:  xpord3pred  8134  unblem1  9291  fin23lem26  10316  fin23lem29  10332  isf32lem8  10351  fprodfvdvdsd  16273  mrieqvlemd  17569  mrieqv2d  17579  mrissmrid  17581  mreexmrid  17583  mreexexlem2d  17585  mreexexlem4d  17587  acsfiindd  18502  ablfac1eulem  19936  cntzsdrg  20410  lbspss  20685  lspsolv  20748  lsppratlem3  20754  lsppratlem4  20755  lspprat  20758  islbs2  20759  islbs3  20760  lbsextlem2  20764  lbsextlem3  20765  lbsextlem4  20766  lpss3  22639  islp3  22641  neitr  22675  restlp  22678  lpcls  22859  qtoprest  23212  ufinffr  23424  cldsubg  23606  xrge0gsumle  24340  bcthlem5  24836  rrxmval  24913  cmmbl  25042  nulmbl2  25044  shftmbl  25046  iundisj2  25057  uniiccdif  25086  uniiccmbl  25098  itg1val2  25192  itg1cl  25193  itg1ge0  25194  i1fadd  25203  itg1addlem5  25209  i1fmulc  25212  itg1mulc  25213  itg10a  25219  itg1ge0a  25220  itg1climres  25223  mbfi1fseqlem4  25227  itgss3  25323  limcdif  25384  limcnlp  25386  limcmpt2  25392  perfdvf  25411  dvcnp2  25428  dvaddbr  25446  dvmulbr  25447  dvferm1  25493  dvferm2  25495  ftc1lem6  25549  ig1peu  25680  ig1pdvds  25685  taylthlem1  25876  taylthlem2  25877  ulmdvlem3  25905  rlimcnp  26459  wilthlem2  26562  newf  27342  elpwdifcl  31751  iundisj2f  31808  ofpreima2  31878  iundisj2fi  31995  tocyccntz  32290  0nellinds  32471  elrspunidl  32534  ig1pmindeg  32659  lindsunlem  32697  lbsdiflsp0  32699  omsmeas  33310  eulerpartlemgs2  33367  ballotlemfrc  33513  hgt750lemd  33648  hgt750leme  33658  cvmscld  34252  gg-dvcnp2  35162  gg-dvmulbr  35163  unbdqndv1  35372  lindsadd  36469  lindsenlbs  36471  ftc1cnnc  36548  lsatfixedN  37867  dochsnkr  40331  hdmaprnlem4tN  40711  prjcrv0  41371  supminfxr2  44165  limcrecl  44331  cnrefiisplem  44531  fperdvper  44621  ismbl3  44688  ovolsplit  44690  ismbl4  44695  stoweidlem57  44759  dirkercncflem3  44807  fourierdlem42  44851  fourierdlem46  44854  fourierdlem62  44870  caragenuncllem  45214  caragendifcl  45216  omelesplit  45220  carageniuncllem2  45224  carageniuncl  45225  caragenel2d  45234  hspmbllem3  45330  hspmbl  45331  ovnsplit  45350  vonvolmbllem  45362  vonvolmbl  45363  c0rnghm  46697  lincdifsn  47058  lindslinindsimp1  47091  lincresunit3lem2  47114