Theorem ssdifssd 4083

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895   ∖ cdif 4045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-dif 4047

This theorem is used by:  xpord3pred  8169  unblem1  9284  fin23lem26  10403  fin23lem29  10419  isf32lem8  10438  fprodfvdvdsd  16504  mrieqvlemd  17803  mrieqv2d  17813  mrissmrid  17815  mreexmrid  17817  mreexexlem2d  17819  mreexexlem4d  17821  acsfiindd  18727  ablfac1eulem  20288  c0rnghm  20787  cntzsdrg  21059  lbspss  21357  lspsolv  21421  lsppratlem3  21427  lsppratlem4  21428  lspprat  21431  islbs2  21432  islbs3  21433  lbsextlem2  21437  lbsextlem3  21438  lbsextlem4  21439  lindsenlbs  22157  lpss3  23462  islp3  23464  neitr  23498  restlp  23501  lpcls  23682  qtoprest  24036  ufinffr  24248  cldsubg  24430  xrge0gsumle  25153  bcthlem5  25649  rrxmval  25726  cmmbl  25855  nulmbl2  25857  shftmbl  25859  iundisj2  25870  uniiccdif  25899  uniiccmbl  25911  itg1val2  26005  itg1cl  26006  itg1ge0  26007  i1fadd  26016  itg1addlem5  26021  i1fmulc  26024  itg1mulc  26025  itg10a  26031  itg1ge0a  26032  itg1climres  26035  mbfi1fseqlem4  26039  itgss3  26135  limcdif  26196  limcnlp  26198  limcmpt2  26204  perfdvf  26223  dvcnp2  26240  dvaddbr  26258  dvmulbr  26259  dvferm1  26305  dvferm2  26307  ftc1lem6  26361  ig1peu  26493  ig1pdvds  26498  taylthlem1  26700  taylthlem2  26701  ulmdvlem3  26729  rlimcnp  27293  wilthlem2  27396  newf  28224  elpwdifcl  33122  iundisj2f  33184  ofpreima2  33260  iundisj2fi  33389  tocyccntz  33705  fxpsdrg  33736  elrgspnsubrunlem1  33808  elrgspnsubrunlem2  33809  0nellinds  33926  elrspunidl  33978  rprmdvdsprod  34066  ig1pmindeg  34134  lindsunlem  34256  lbsdiflsp0  34258  dimlssid  34264  fldextrspunlsp  34306  omsmeas  34955  eulerpartlemgs2  35012  ballotlemfrc  35159  hgt750lemd  35277  hgt750leme  35287  cvmscld  36038  unbdqndv1  37374  lindsadd  38537  ftc1cnnc  38611  lsatfixedN  40067  dochsnkr  42530  hdmaprnlem4tN  42910  redvmptabs  43412  prjcrv0  43670  supminfxr2  46479  limcrecl  46641  cnrefiisplem  46839  fperdvper  46929  ismbl3  46996  ovolsplit  46998  ismbl4  47003  stoweidlem57  47067  dirkercncflem3  47115  fourierdlem42  47159  fourierdlem46  47162  fourierdlem62  47178  caragenuncllem  47522  caragendifcl  47524  omelesplit  47528  carageniuncllem2  47532  carageniuncl  47533  caragenel2d  47542  hspmbllem3  47638  hspmbl  47639  ovnsplit  47658  vonvolmbllem  47670  vonvolmbl  47671  lincdifsn  49536  lindslinindsimp1  49569  lincresunit3lem2  49592