Theorem ssdifssd 4078

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

Syntax hints:   → wi 4   ∖ cdif 3885   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-dif 3891  df-in 3895  df-ss 3905

This theorem is referenced by:  unblem1  9075  fin23lem26  10090  fin23lem29  10106  isf32lem8  10125  fprodfvdvdsd  16052  mrieqvlemd  17347  mrieqv2d  17357  mrissmrid  17359  mreexmrid  17361  mreexexlem2d  17363  mreexexlem4d  17365  acsfiindd  18280  ablfac1eulem  19684  cntzsdrg  20079  lbspss  20353  lspsolv  20414  lsppratlem3  20420  lsppratlem4  20421  lspprat  20424  islbs2  20425  islbs3  20426  lbsextlem2  20430  lbsextlem3  20431  lbsextlem4  20432  lpss3  22304  islp3  22306  neitr  22340  restlp  22343  lpcls  22524  qtoprest  22877  ufinffr  23089  cldsubg  23271  xrge0gsumle  24005  bcthlem5  24501  rrxmval  24578  cmmbl  24707  nulmbl2  24709  shftmbl  24711  iundisj2  24722  uniiccdif  24751  uniiccmbl  24763  itg1val2  24857  itg1cl  24858  itg1ge0  24859  i1fadd  24868  itg1addlem5  24874  i1fmulc  24877  itg1mulc  24878  itg10a  24884  itg1ge0a  24885  itg1climres  24888  mbfi1fseqlem4  24892  itgss3  24988  limcdif  25049  limcnlp  25051  limcmpt2  25057  perfdvf  25076  dvcnp2  25093  dvaddbr  25111  dvmulbr  25112  dvferm1  25158  dvferm2  25160  ftc1lem6  25214  ig1peu  25345  ig1pdvds  25350  taylthlem1  25541  taylthlem2  25542  ulmdvlem3  25570  rlimcnp  26124  wilthlem2  26227  elpwdifcl  30884  iundisj2f  30938  ofpreima2  31012  iundisj2fi  31127  tocyccntz  31420  0nellinds  31575  elrspunidl  31615  lindsunlem  31714  lbsdiflsp0  31716  omsmeas  32299  eulerpartlemgs2  32356  ballotlemfrc  32502  hgt750lemd  32637  hgt750leme  32647  cvmscld  33244  xpord3pred  33807  newf  34051  unbdqndv1  34697  lindsadd  35779  lindsenlbs  35781  ftc1cnnc  35858  lsatfixedN  37030  dochsnkr  39493  hdmaprnlem4tN  39873  supminfxr2  43016  limcrecl  43177  cnrefiisplem  43377  fperdvper  43467  ismbl3  43534  ovolsplit  43536  ismbl4  43541  stoweidlem57  43605  dirkercncflem3  43653  fourierdlem42  43697  fourierdlem46  43700  fourierdlem62  43716  caragenuncllem  44057  caragendifcl  44059  omelesplit  44063  carageniuncllem2  44067  carageniuncl  44068  caragenel2d  44077  hspmbllem3  44173  hspmbl  44174  ovnsplit  44193  vonvolmbllem  44205  vonvolmbl  44206  c0rnghm  45482  lincdifsn  45776  lindslinindsimp1  45809  lincresunit3lem2  45832