Theorem ssdifssd 4134

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

Syntax hints:   → wi 4   ∖ cdif 3937   ⊆ wss 3940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-dif 3943  df-in 3947  df-ss 3957

This theorem is referenced by:  xpord3pred  8132  unblem1  9291  fin23lem26  10316  fin23lem29  10332  isf32lem8  10351  fprodfvdvdsd  16274  mrieqvlemd  17572  mrieqv2d  17582  mrissmrid  17584  mreexmrid  17586  mreexexlem2d  17588  mreexexlem4d  17590  acsfiindd  18508  ablfac1eulem  19984  c0rnghm  20425  cntzsdrg  20643  lbspss  20920  lspsolv  20984  lsppratlem3  20990  lsppratlem4  20991  lspprat  20994  islbs2  20995  islbs3  20996  lbsextlem2  21000  lbsextlem3  21001  lbsextlem4  21002  lpss3  22970  islp3  22972  neitr  23006  restlp  23009  lpcls  23190  qtoprest  23543  ufinffr  23755  cldsubg  23937  xrge0gsumle  24671  bcthlem5  25178  rrxmval  25255  cmmbl  25385  nulmbl2  25387  shftmbl  25389  iundisj2  25400  uniiccdif  25429  uniiccmbl  25441  itg1val2  25535  itg1cl  25536  itg1ge0  25537  i1fadd  25546  itg1addlem5  25552  i1fmulc  25555  itg1mulc  25556  itg10a  25562  itg1ge0a  25563  itg1climres  25566  mbfi1fseqlem4  25570  itgss3  25666  limcdif  25727  limcnlp  25729  limcmpt2  25735  perfdvf  25754  dvcnp2  25771  dvcnp2OLD  25772  dvaddbr  25790  dvmulbr  25791  dvmulbrOLD  25792  dvferm1  25839  dvferm2  25841  ftc1lem6  25898  ig1peu  26029  ig1pdvds  26034  taylthlem1  26226  taylthlem2  26227  ulmdvlem3  26255  rlimcnp  26813  wilthlem2  26917  newf  27701  elpwdifcl  32233  iundisj2f  32290  ofpreima2  32360  iundisj2fi  32477  tocyccntz  32771  0nellinds  32952  elrspunidl  33015  ig1pmindeg  33138  lindsunlem  33188  lbsdiflsp0  33190  omsmeas  33811  eulerpartlemgs2  33868  ballotlemfrc  34014  hgt750lemd  34149  hgt750leme  34159  cvmscld  34753  gg-taylthlem2  35657  unbdqndv1  35874  lindsadd  36971  lindsenlbs  36973  ftc1cnnc  37050  lsatfixedN  38369  dochsnkr  40833  hdmaprnlem4tN  41213  prjcrv0  41864  supminfxr2  44664  limcrecl  44830  cnrefiisplem  45030  fperdvper  45120  ismbl3  45187  ovolsplit  45189  ismbl4  45194  stoweidlem57  45258  dirkercncflem3  45306  fourierdlem42  45350  fourierdlem46  45353  fourierdlem62  45369  caragenuncllem  45713  caragendifcl  45715  omelesplit  45719  carageniuncllem2  45723  carageniuncl  45724  caragenel2d  45733  hspmbllem3  45829  hspmbl  45830  ovnsplit  45849  vonvolmbllem  45861  vonvolmbl  45862  lincdifsn  47293  lindslinindsimp1  47326  lincresunit3lem2  47349