Theorem ssdifssd 4088

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

Syntax hints:   → wi 4   ∖ cdif 3887   ⊆ wss 3890

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-ss 3907

This theorem is referenced by:  xpord3pred  8097  unblem1  9197  fin23lem26  10242  fin23lem29  10258  isf32lem8  10277  fprodfvdvdsd  16298  mrieqvlemd  17590  mrieqv2d  17600  mrissmrid  17602  mreexmrid  17604  mreexexlem2d  17606  mreexexlem4d  17608  acsfiindd  18514  ablfac1eulem  20044  c0rnghm  20507  cntzsdrg  20774  lbspss  21073  lspsolv  21137  lsppratlem3  21143  lsppratlem4  21144  lspprat  21147  islbs2  21148  islbs3  21149  lbsextlem2  21153  lbsextlem3  21154  lbsextlem4  21155  lpss3  23123  islp3  23125  neitr  23159  restlp  23162  lpcls  23343  qtoprest  23696  ufinffr  23908  cldsubg  24090  xrge0gsumle  24813  bcthlem5  25309  rrxmval  25386  cmmbl  25515  nulmbl2  25517  shftmbl  25519  iundisj2  25530  uniiccdif  25559  uniiccmbl  25571  itg1val2  25665  itg1cl  25666  itg1ge0  25667  i1fadd  25676  itg1addlem5  25681  i1fmulc  25684  itg1mulc  25685  itg10a  25691  itg1ge0a  25692  itg1climres  25695  mbfi1fseqlem4  25699  itgss3  25796  limcdif  25857  limcnlp  25859  limcmpt2  25865  perfdvf  25884  dvcnp2  25901  dvaddbr  25919  dvmulbr  25920  dvferm1  25966  dvferm2  25968  ftc1lem6  26022  ig1peu  26154  ig1pdvds  26159  taylthlem1  26354  taylthlem2  26355  taylthlem2OLD  26356  ulmdvlem3  26384  rlimcnp  26946  wilthlem2  27050  newf  27848  elpwdifcl  32615  iundisj2f  32679  ofpreima2  32758  iundisj2fi  32889  tocyccntz  33224  fxpsdrg  33255  elrgspnsubrunlem1  33327  elrgspnsubrunlem2  33328  0nellinds  33449  elrspunidl  33507  rprmdvdsprod  33613  ig1pmindeg  33681  lindsunlem  33788  lbsdiflsp0  33790  dimlssid  33796  fldextrspunlsp  33838  omsmeas  34487  eulerpartlemgs2  34544  ballotlemfrc  34691  hgt750lemd  34812  hgt750leme  34822  cvmscld  35475  unbdqndv1  36788  lindsadd  37952  lindsenlbs  37954  ftc1cnnc  38031  lsatfixedN  39473  dochsnkr  41936  hdmaprnlem4tN  42316  redvmptabs  42810  prjcrv0  43084  supminfxr2  45919  limcrecl  46081  cnrefiisplem  46279  fperdvper  46369  ismbl3  46436  ovolsplit  46438  ismbl4  46443  stoweidlem57  46507  dirkercncflem3  46555  fourierdlem42  46599  fourierdlem46  46602  fourierdlem62  46618  caragenuncllem  46962  caragendifcl  46964  omelesplit  46968  carageniuncllem2  46972  carageniuncl  46973  caragenel2d  46982  hspmbllem3  47078  hspmbl  47079  ovnsplit  47098  vonvolmbllem  47110  vonvolmbl  47111  lincdifsn  48916  lindslinindsimp1  48949  lincresunit3lem2  48972