Theorem ssdifssd 4147

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

Syntax hints:   → wi 4   ∖ cdif 3948   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-ss 3968

This theorem is referenced by:  xpord3pred  8177  unblem1  9328  fin23lem26  10365  fin23lem29  10381  isf32lem8  10400  fprodfvdvdsd  16371  mrieqvlemd  17672  mrieqv2d  17682  mrissmrid  17684  mreexmrid  17686  mreexexlem2d  17688  mreexexlem4d  17690  acsfiindd  18598  ablfac1eulem  20092  c0rnghm  20535  cntzsdrg  20803  lbspss  21081  lspsolv  21145  lsppratlem3  21151  lsppratlem4  21152  lspprat  21155  islbs2  21156  islbs3  21157  lbsextlem2  21161  lbsextlem3  21162  lbsextlem4  21163  lpss3  23152  islp3  23154  neitr  23188  restlp  23191  lpcls  23372  qtoprest  23725  ufinffr  23937  cldsubg  24119  xrge0gsumle  24855  bcthlem5  25362  rrxmval  25439  cmmbl  25569  nulmbl2  25571  shftmbl  25573  iundisj2  25584  uniiccdif  25613  uniiccmbl  25625  itg1val2  25719  itg1cl  25720  itg1ge0  25721  i1fadd  25730  itg1addlem5  25735  i1fmulc  25738  itg1mulc  25739  itg10a  25745  itg1ge0a  25746  itg1climres  25749  mbfi1fseqlem4  25753  itgss3  25850  limcdif  25911  limcnlp  25913  limcmpt2  25919  perfdvf  25938  dvcnp2  25955  dvcnp2OLD  25956  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvferm1  26023  dvferm2  26025  ftc1lem6  26082  ig1peu  26214  ig1pdvds  26219  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmdvlem3  26445  rlimcnp  27008  wilthlem2  27112  newf  27897  elpwdifcl  32545  iundisj2f  32603  ofpreima2  32676  iundisj2fi  32799  tocyccntz  33164  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  0nellinds  33398  elrspunidl  33456  rprmdvdsprod  33562  ig1pmindeg  33622  lindsunlem  33675  lbsdiflsp0  33677  dimlssid  33683  fldextrspunlsp  33724  omsmeas  34325  eulerpartlemgs2  34382  ballotlemfrc  34529  hgt750lemd  34663  hgt750leme  34673  cvmscld  35278  unbdqndv1  36509  lindsadd  37620  lindsenlbs  37622  ftc1cnnc  37699  lsatfixedN  39010  dochsnkr  41474  hdmaprnlem4tN  41854  redvmptabs  42390  prjcrv0  42643  supminfxr2  45480  limcrecl  45644  cnrefiisplem  45844  fperdvper  45934  ismbl3  46001  ovolsplit  46003  ismbl4  46008  stoweidlem57  46072  dirkercncflem3  46120  fourierdlem42  46164  fourierdlem46  46167  fourierdlem62  46183  caragenuncllem  46527  caragendifcl  46529  omelesplit  46533  carageniuncllem2  46537  carageniuncl  46538  caragenel2d  46547  hspmbllem3  46643  hspmbl  46644  ovnsplit  46663  vonvolmbllem  46675  vonvolmbl  46676  lincdifsn  48341  lindslinindsimp1  48374  lincresunit3lem2  48397