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 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ 𝐵)

Syntax hints:   → wi 4   ∖ cdif 3900   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-ss 3920

This theorem is referenced by:  xpord3pred  8106  unblem1  9206  fin23lem26  10249  fin23lem29  10265  isf32lem8  10284  fprodfvdvdsd  16275  mrieqvlemd  17566  mrieqv2d  17576  mrissmrid  17578  mreexmrid  17580  mreexexlem2d  17582  mreexexlem4d  17584  acsfiindd  18490  ablfac1eulem  20020  c0rnghm  20485  cntzsdrg  20752  lbspss  21051  lspsolv  21115  lsppratlem3  21121  lsppratlem4  21122  lspprat  21125  islbs2  21126  islbs3  21127  lbsextlem2  21131  lbsextlem3  21132  lbsextlem4  21133  lpss3  23105  islp3  23107  neitr  23141  restlp  23144  lpcls  23325  qtoprest  23678  ufinffr  23890  cldsubg  24072  xrge0gsumle  24795  bcthlem5  25301  rrxmval  25378  cmmbl  25508  nulmbl2  25510  shftmbl  25512  iundisj2  25523  uniiccdif  25552  uniiccmbl  25564  itg1val2  25658  itg1cl  25659  itg1ge0  25660  i1fadd  25669  itg1addlem5  25674  i1fmulc  25677  itg1mulc  25678  itg10a  25684  itg1ge0a  25685  itg1climres  25688  mbfi1fseqlem4  25692  itgss3  25789  limcdif  25850  limcnlp  25852  limcmpt2  25858  perfdvf  25877  dvcnp2  25894  dvcnp2OLD  25895  dvaddbr  25913  dvmulbr  25914  dvmulbrOLD  25915  dvferm1  25962  dvferm2  25964  ftc1lem6  26021  ig1peu  26153  ig1pdvds  26158  taylthlem1  26354  taylthlem2  26355  taylthlem2OLD  26356  ulmdvlem3  26384  rlimcnp  26948  wilthlem2  27052  newf  27851  elpwdifcl  32619  iundisj2f  32683  ofpreima2  32762  iundisj2fi  32894  tocyccntz  33244  fxpsdrg  33275  elrgspnsubrunlem1  33347  elrgspnsubrunlem2  33348  0nellinds  33469  elrspunidl  33527  rprmdvdsprod  33633  ig1pmindeg  33701  lindsunlem  33808  lbsdiflsp0  33810  dimlssid  33816  fldextrspunlsp  33858  omsmeas  34507  eulerpartlemgs2  34564  ballotlemfrc  34711  hgt750lemd  34832  hgt750leme  34842  cvmscld  35495  unbdqndv1  36736  lindsadd  37893  lindsenlbs  37895  ftc1cnnc  37972  lsatfixedN  39414  dochsnkr  41877  hdmaprnlem4tN  42257  redvmptabs  42759  prjcrv0  43020  supminfxr2  45856  limcrecl  46018  cnrefiisplem  46216  fperdvper  46306  ismbl3  46373  ovolsplit  46375  ismbl4  46380  stoweidlem57  46444  dirkercncflem3  46492  fourierdlem42  46536  fourierdlem46  46539  fourierdlem62  46555  caragenuncllem  46899  caragendifcl  46901  omelesplit  46905  carageniuncllem2  46909  carageniuncl  46910  caragenel2d  46919  hspmbllem3  47015  hspmbl  47016  ovnsplit  47035  vonvolmbllem  47047  vonvolmbl  47048  lincdifsn  48813  lindslinindsimp1  48846  lincresunit3lem2  48869