Theorem ssdifssd 4109

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

Syntax hints:   → wi 4   ∖ cdif 3910   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-ss 3930

This theorem is referenced by:  xpord3pred  8148  unblem1  9252  fin23lem26  10309  fin23lem29  10325  isf32lem8  10344  fprodfvdvdsd  16392  mrieqvlemd  17685  mrieqv2d  17695  mrissmrid  17697  mreexmrid  17699  mreexexlem2d  17701  mreexexlem4d  17703  acsfiindd  18609  ablfac1eulem  20144  c0rnghm  20620  cntzsdrg  20883  lbspss  21181  lspsolv  21245  lsppratlem3  21251  lsppratlem4  21252  lspprat  21255  islbs2  21256  islbs3  21257  lbsextlem2  21261  lbsextlem3  21262  lbsextlem4  21263  lpss3  23270  islp3  23272  neitr  23306  restlp  23309  lpcls  23490  qtoprest  23843  ufinffr  24055  cldsubg  24237  xrge0gsumle  24960  bcthlem5  25456  rrxmval  25533  cmmbl  25662  nulmbl2  25664  shftmbl  25666  iundisj2  25677  uniiccdif  25706  uniiccmbl  25718  itg1val2  25812  itg1cl  25813  itg1ge0  25814  i1fadd  25823  itg1addlem5  25828  i1fmulc  25831  itg1mulc  25832  itg10a  25838  itg1ge0a  25839  itg1climres  25842  mbfi1fseqlem4  25846  itgss3  25943  limcdif  26004  limcnlp  26006  limcmpt2  26012  perfdvf  26031  dvcnp2  26048  dvaddbr  26066  dvmulbr  26067  dvferm1  26113  dvferm2  26115  ftc1lem6  26169  ig1peu  26301  ig1pdvds  26306  taylthlem1  26502  taylthlem2  26503  ulmdvlem3  26531  rlimcnp  27096  wilthlem2  27199  newf  27997  elpwdifcl  32813  iundisj2f  32876  ofpreima2  32952  iundisj2fi  33083  tocyccntz  33405  fxpsdrg  33436  elrgspnsubrunlem1  33508  elrgspnsubrunlem2  33509  0nellinds  33628  elrspunidl  33680  rprmdvdsprod  33769  ig1pmindeg  33837  lindsunlem  33959  lbsdiflsp0  33961  dimlssid  33967  fldextrspunlsp  34009  omsmeas  34658  eulerpartlemgs2  34715  ballotlemfrc  34862  hgt750lemd  34980  hgt750leme  34990  cvmscld  35698  unbdqndv1  37020  lindsadd  38186  lindsenlbs  38188  ftc1cnnc  38265  lsatfixedN  39707  dochsnkr  42170  hdmaprnlem4tN  42550  redvmptabs  43045  prjcrv0  43291  supminfxr2  46109  limcrecl  46271  cnrefiisplem  46469  fperdvper  46559  ismbl3  46626  ovolsplit  46628  ismbl4  46633  stoweidlem57  46697  dirkercncflem3  46745  fourierdlem42  46789  fourierdlem46  46792  fourierdlem62  46808  caragenuncllem  47152  caragendifcl  47154  omelesplit  47158  carageniuncllem2  47162  carageniuncl  47163  caragenel2d  47172  hspmbllem3  47268  hspmbl  47269  ovnsplit  47288  vonvolmbllem  47300  vonvolmbl  47301  lincdifsn  49123  lindslinindsimp1  49156  lincresunit3lem2  49179