Theorem ssdifssd 3710

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

Syntax hints:   → wi 4   ∖ cdif 3537   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554

This theorem is referenced by:  unblem1  8097  fin23lem26  9030  fin23lem29  9046  isf32lem8  9065  fprodfvdvdsd  14896  mrieqvlemd  16112  mrieqv2d  16122  mrissmrid  16124  mreexmrid  16126  mreexexlem2d  16128  mreexexlem4d  16130  acsfiindd  17000  ablfac1eulem  18294  lbspss  18903  lspsolv  18964  lsppratlem3  18970  lsppratlem4  18971  lspprat  18974  islbs2  18975  islbs3  18976  lbsextlem2  18980  lbsextlem3  18981  lbsextlem4  18982  lpss3  20758  islp3  20760  neitr  20794  restlp  20797  lpcls  20978  qtoprest  21330  ufinffr  21543  cldsubg  21724  xrge0gsumle  22444  bcthlem5  22933  rrxmval  22996  cmmbl  23109  nulmbl2  23111  shftmbl  23113  iundisj2  23124  uniiccdif  23152  uniiccmbl  23164  itg1val2  23257  itg1cl  23258  itg1ge0  23259  i1fadd  23268  itg1addlem5  23273  i1fmulc  23276  itg1mulc  23277  itg10a  23283  itg1ge0a  23284  itg1climres  23287  mbfi1fseqlem4  23291  itgss3  23387  limcdif  23446  limcnlp  23448  limcmpt2  23454  perfdvf  23473  dvcnp2  23489  dvaddbr  23507  dvmulbr  23508  dvferm1  23552  dvferm2  23554  ftc1lem6  23608  ig1peu  23735  ig1pdvds  23740  taylthlem1  23931  taylthlem2  23932  ulmdvlem3  23960  rlimcnp  24492  wilthlem2  24595  elpwdifcl  28742  iundisj2f  28785  ofpreima2  28849  iundisj2fi  28943  omsmeas  29712  eulerpartlemgs2  29769  ballotlemfrc  29915  cvmscld  30509  unbdqndv1  31669  lindsenlbs  32574  ftc1cnnc  32654  lsatfixedN  33314  dochsnkr  35779  hdmaprnlem4tN  36162  cntzsdrg  36791  limcrecl  38696  fperdvper  38808  ismbl3  38879  ovolsplit  38881  ismbl4  38886  stoweidlem57  38950  dirkercncflem3  38998  fourierdlem42  39042  fourierdlem46  39045  fourierdlem62  39061  caragenuncllem  39402  caragendifcl  39404  omelesplit  39408  carageniuncllem2  39412  carageniuncl  39413  caragenel2d  39422  hspmbllem3  39518  hspmbl  39519  ovnsplit  39538  vonvolmbllem  39550  vonvolmbl  39551  c0rnghm  41703  lincdifsn  42007  lindslinindsimp1  42040  lincresunit3lem2  42063