Theorem ssdifssd 4086

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900   ∖ cdif 4048

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-dif 4050

This theorem is used by:  xpord3pred  8193  unblem1  9309  fin23lem26  10427  fin23lem29  10443  isf32lem8  10462  fprodfvdvdsd  16530  mrieqvlemd  17829  mrieqv2d  17839  mrissmrid  17841  mreexmrid  17843  mreexexlem2d  17845  mreexexlem4d  17847  acsfiindd  18753  ablfac1eulem  20315  c0rnghm  20814  cntzsdrg  21086  lbspss  21384  lspsolv  21448  lsppratlem3  21454  lsppratlem4  21455  lspprat  21458  islbs2  21459  islbs3  21460  lbsextlem2  21464  lbsextlem3  21465  lbsextlem4  21466  lindsenlbs  22184  lpss3  23489  islp3  23491  neitr  23525  restlp  23528  lpcls  23709  qtoprest  24063  ufinffr  24275  cldsubg  24457  xrge0gsumle  25180  bcthlem5  25676  rrxmval  25753  cmmbl  25882  nulmbl2  25884  shftmbl  25886  iundisj2  25897  uniiccdif  25926  uniiccmbl  25938  itg1val2  26032  itg1cl  26033  itg1ge0  26034  i1fadd  26043  itg1addlem5  26048  i1fmulc  26051  itg1mulc  26052  itg10a  26058  itg1ge0a  26059  itg1climres  26062  mbfi1fseqlem4  26066  itgss3  26162  limcdif  26223  limcnlp  26225  limcmpt2  26231  perfdvf  26250  dvcnp2  26267  dvaddbr  26285  dvmulbr  26286  dvferm1  26332  dvferm2  26334  ftc1lem6  26388  ig1peu  26520  ig1pdvds  26525  taylthlem1  26727  taylthlem2  26728  ulmdvlem3  26756  rlimcnp  27320  wilthlem2  27423  newf  28251  elpwdifcl  33191  iundisj2f  33253  ofpreima2  33329  iundisj2fi  33456  tocyccntz  33772  fxpsdrg  33803  elrgspnsubrunlem1  33875  elrgspnsubrunlem2  33876  0nellinds  33993  elrspunidl  34045  rprmdvdsprod  34133  ig1pmindeg  34201  lindsunlem  34323  lbsdiflsp0  34325  dimlssid  34331  fldextrspunlsp  34373  omsmeas  35022  eulerpartlemgs2  35079  ballotlemfrc  35226  hgt750lemd  35344  hgt750leme  35354  cvmscld  36204  unbdqndv1  37551  lindsadd  38727  ftc1cnnc  38801  lsatfixedN  40257  dochsnkr  42720  hdmaprnlem4tN  43100  redvmptabs  43602  prjcrv0  43860  supminfxr2  46682  limcrecl  46844  cnrefiisplem  47042  fperdvper  47132  ismbl3  47199  ovolsplit  47201  ismbl4  47206  stoweidlem57  47270  dirkercncflem3  47318  fourierdlem42  47362  fourierdlem46  47365  fourierdlem62  47381  caragenuncllem  47725  caragendifcl  47727  omelesplit  47731  carageniuncllem2  47735  carageniuncl  47736  caragenel2d  47745  hspmbllem3  47841  hspmbl  47842  ovnsplit  47861  vonvolmbllem  47873  vonvolmbl  47874  lincdifsn  49739  lindslinindsimp1  49772  lincresunit3lem2  49795