Theorem ssdifssd 4080

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-dif 3888  df-ss 3902

This theorem is referenced by:  xpord3pred  8096  unblem1  9196  fin23lem26  10242  fin23lem29  10258  isf32lem8  10277  fprodfvdvdsd  16298  mrieqvlemd  17590  mrieqv2d  17600  mrissmrid  17602  mreexmrid  17604  mreexexlem2d  17606  mreexexlem4d  17608  acsfiindd  18514  ablfac1eulem  20044  c0rnghm  20511  cntzsdrg  20778  lbspss  21076  lspsolv  21140  lsppratlem3  21146  lsppratlem4  21147  lspprat  21150  islbs2  21151  islbs3  21152  lbsextlem2  21156  lbsextlem3  21157  lbsextlem4  21158  lpss3  23131  islp3  23133  neitr  23167  restlp  23170  lpcls  23351  qtoprest  23704  ufinffr  23916  cldsubg  24098  xrge0gsumle  24821  bcthlem5  25317  rrxmval  25394  cmmbl  25523  nulmbl2  25525  shftmbl  25527  iundisj2  25538  uniiccdif  25567  uniiccmbl  25579  itg1val2  25673  itg1cl  25674  itg1ge0  25675  i1fadd  25684  itg1addlem5  25689  i1fmulc  25692  itg1mulc  25693  itg10a  25699  itg1ge0a  25700  itg1climres  25703  mbfi1fseqlem4  25707  itgss3  25804  limcdif  25865  limcnlp  25867  limcmpt2  25873  perfdvf  25892  dvcnp2  25909  dvaddbr  25927  dvmulbr  25928  dvferm1  25974  dvferm2  25976  ftc1lem6  26030  ig1peu  26162  ig1pdvds  26167  taylthlem1  26360  taylthlem2  26361  ulmdvlem3  26389  rlimcnp  26951  wilthlem2  27054  newf  27852  elpwdifcl  32618  iundisj2f  32683  ofpreima2  32762  iundisj2fi  32893  tocyccntz  33229  fxpsdrg  33260  elrgspnsubrunlem1  33332  elrgspnsubrunlem2  33333  0nellinds  33457  elrspunidl  33515  rprmdvdsprod  33629  ig1pmindeg  33697  lindsunlem  33820  lbsdiflsp0  33822  dimlssid  33828  fldextrspunlsp  33870  omsmeas  34519  eulerpartlemgs2  34576  ballotlemfrc  34723  hgt750lemd  34844  hgt750leme  34854  cvmscld  35516  unbdqndv1  36829  lindsadd  37995  lindsenlbs  37997  ftc1cnnc  38074  lsatfixedN  39516  dochsnkr  41979  hdmaprnlem4tN  42359  redvmptabs  42852  prjcrv0  43098  supminfxr2  45926  limcrecl  46088  cnrefiisplem  46286  fperdvper  46376  ismbl3  46443  ovolsplit  46445  ismbl4  46450  stoweidlem57  46514  dirkercncflem3  46562  fourierdlem42  46606  fourierdlem46  46609  fourierdlem62  46625  caragenuncllem  46969  caragendifcl  46971  omelesplit  46975  carageniuncllem2  46979  carageniuncl  46980  caragenel2d  46989  hspmbllem3  47085  hspmbl  47086  ovnsplit  47105  vonvolmbllem  47117  vonvolmbl  47118  lincdifsn  48929  lindslinindsimp1  48962  lincresunit3lem2  48985