Theorem ssdifssd 4113

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

Syntax hints:   → wi 4   ∖ cdif 3914   ⊆ wss 3917

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-ss 3934

This theorem is referenced by:  xpord3pred  8134  unblem1  9246  fin23lem26  10285  fin23lem29  10301  isf32lem8  10320  fprodfvdvdsd  16311  mrieqvlemd  17597  mrieqv2d  17607  mrissmrid  17609  mreexmrid  17611  mreexexlem2d  17613  mreexexlem4d  17615  acsfiindd  18519  ablfac1eulem  20011  c0rnghm  20451  cntzsdrg  20718  lbspss  20996  lspsolv  21060  lsppratlem3  21066  lsppratlem4  21067  lspprat  21070  islbs2  21071  islbs3  21072  lbsextlem2  21076  lbsextlem3  21077  lbsextlem4  21078  lpss3  23038  islp3  23040  neitr  23074  restlp  23077  lpcls  23258  qtoprest  23611  ufinffr  23823  cldsubg  24005  xrge0gsumle  24729  bcthlem5  25235  rrxmval  25312  cmmbl  25442  nulmbl2  25444  shftmbl  25446  iundisj2  25457  uniiccdif  25486  uniiccmbl  25498  itg1val2  25592  itg1cl  25593  itg1ge0  25594  i1fadd  25603  itg1addlem5  25608  i1fmulc  25611  itg1mulc  25612  itg10a  25618  itg1ge0a  25619  itg1climres  25622  mbfi1fseqlem4  25626  itgss3  25723  limcdif  25784  limcnlp  25786  limcmpt2  25792  perfdvf  25811  dvcnp2  25828  dvcnp2OLD  25829  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvferm1  25896  dvferm2  25898  ftc1lem6  25955  ig1peu  26087  ig1pdvds  26092  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulmdvlem3  26318  rlimcnp  26882  wilthlem2  26986  newf  27773  elpwdifcl  32462  iundisj2f  32526  ofpreima2  32597  iundisj2fi  32727  tocyccntz  33108  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  0nellinds  33348  elrspunidl  33406  rprmdvdsprod  33512  ig1pmindeg  33574  lindsunlem  33627  lbsdiflsp0  33629  dimlssid  33635  fldextrspunlsp  33676  omsmeas  34321  eulerpartlemgs2  34378  ballotlemfrc  34525  hgt750lemd  34646  hgt750leme  34656  cvmscld  35267  unbdqndv1  36503  lindsadd  37614  lindsenlbs  37616  ftc1cnnc  37693  lsatfixedN  39009  dochsnkr  41473  hdmaprnlem4tN  41853  redvmptabs  42355  prjcrv0  42628  supminfxr2  45472  limcrecl  45634  cnrefiisplem  45834  fperdvper  45924  ismbl3  45991  ovolsplit  45993  ismbl4  45998  stoweidlem57  46062  dirkercncflem3  46110  fourierdlem42  46154  fourierdlem46  46157  fourierdlem62  46173  caragenuncllem  46517  caragendifcl  46519  omelesplit  46523  carageniuncllem2  46527  carageniuncl  46528  caragenel2d  46537  hspmbllem3  46633  hspmbl  46634  ovnsplit  46653  vonvolmbllem  46665  vonvolmbl  46666  lincdifsn  48417  lindslinindsimp1  48450  lincresunit3lem2  48473