Theorem ssdifssd 4101

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

This proof depends on syntax axioms:   → wi 4   ∖ cdif 3902   ⊆ wss 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-ss 3922

This theorem is used by:  xpord3pred  8144  unblem1  9248  fin23lem26  10313  fin23lem29  10329  isf32lem8  10348  fprodfvdvdsd  16396  mrieqvlemd  17689  mrieqv2d  17699  mrissmrid  17701  mreexmrid  17703  mreexexlem2d  17705  mreexexlem4d  17707  acsfiindd  18613  ablfac1eulem  20148  c0rnghm  20643  cntzsdrg  20914  lbspss  21212  lspsolv  21276  lsppratlem3  21282  lsppratlem4  21283  lspprat  21286  islbs2  21287  islbs3  21288  lbsextlem2  21292  lbsextlem3  21293  lbsextlem4  21294  lpss3  23310  islp3  23312  neitr  23346  restlp  23349  lpcls  23530  qtoprest  23883  ufinffr  24095  cldsubg  24277  xrge0gsumle  25000  bcthlem5  25496  rrxmval  25573  cmmbl  25702  nulmbl2  25704  shftmbl  25706  iundisj2  25717  uniiccdif  25746  uniiccmbl  25758  itg1val2  25852  itg1cl  25853  itg1ge0  25854  i1fadd  25863  itg1addlem5  25868  i1fmulc  25871  itg1mulc  25872  itg10a  25878  itg1ge0a  25879  itg1climres  25882  mbfi1fseqlem4  25886  itgss3  25983  limcdif  26044  limcnlp  26046  limcmpt2  26052  perfdvf  26071  dvcnp2  26088  dvaddbr  26106  dvmulbr  26107  dvferm1  26153  dvferm2  26155  ftc1lem6  26209  ig1peu  26341  ig1pdvds  26346  taylthlem1  26545  taylthlem2  26546  ulmdvlem3  26574  rlimcnp  27139  wilthlem2  27242  newf  28040  elpwdifcl  32881  iundisj2f  32944  ofpreima2  33020  iundisj2fi  33151  tocyccntz  33473  fxpsdrg  33504  elrgspnsubrunlem1  33576  elrgspnsubrunlem2  33577  0nellinds  33694  elrspunidl  33745  rprmdvdsprod  33833  ig1pmindeg  33901  lindsunlem  34023  lbsdiflsp0  34025  dimlssid  34031  fldextrspunlsp  34073  omsmeas  34722  eulerpartlemgs2  34779  ballotlemfrc  34926  hgt750lemd  35044  hgt750leme  35054  cvmscld  35773  unbdqndv1  37125  lindsadd  38292  lindsenlbs  38294  ftc1cnnc  38371  lsatfixedN  39811  dochsnkr  42274  hdmaprnlem4tN  42654  redvmptabs  43149  prjcrv0  43393  supminfxr2  46211  limcrecl  46373  cnrefiisplem  46571  fperdvper  46661  ismbl3  46728  ovolsplit  46730  ismbl4  46735  stoweidlem57  46799  dirkercncflem3  46847  fourierdlem42  46891  fourierdlem46  46894  fourierdlem62  46910  caragenuncllem  47254  caragendifcl  47256  omelesplit  47260  carageniuncllem2  47264  carageniuncl  47265  caragenel2d  47274  hspmbllem3  47370  hspmbl  47371  ovnsplit  47390  vonvolmbllem  47402  vonvolmbl  47403  lincdifsn  49232  lindslinindsimp1  49265  lincresunit3lem2  49288