Theorem ssdifssd 4118

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

Syntax hints:   → wi 4   ∖ cdif 3932   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3938  df-in 3942  df-ss 3951

This theorem is referenced by:  unblem1  8764  fin23lem26  9741  fin23lem29  9757  isf32lem8  9776  fprodfvdvdsd  15677  mrieqvlemd  16894  mrieqv2d  16904  mrissmrid  16906  mreexmrid  16908  mreexexlem2d  16910  mreexexlem4d  16912  acsfiindd  17781  ablfac1eulem  19188  cntzsdrg  19575  lbspss  19848  lspsolv  19909  lsppratlem3  19915  lsppratlem4  19916  lspprat  19919  islbs2  19920  islbs3  19921  lbsextlem2  19925  lbsextlem3  19926  lbsextlem4  19927  lpss3  21746  islp3  21748  neitr  21782  restlp  21785  lpcls  21966  qtoprest  22319  ufinffr  22531  cldsubg  22713  xrge0gsumle  23435  bcthlem5  23925  rrxmval  24002  cmmbl  24129  nulmbl2  24131  shftmbl  24133  iundisj2  24144  uniiccdif  24173  uniiccmbl  24185  itg1val2  24279  itg1cl  24280  itg1ge0  24281  i1fadd  24290  itg1addlem5  24295  i1fmulc  24298  itg1mulc  24299  itg10a  24305  itg1ge0a  24306  itg1climres  24309  mbfi1fseqlem4  24313  itgss3  24409  limcdif  24468  limcnlp  24470  limcmpt2  24476  perfdvf  24495  dvcnp2  24511  dvaddbr  24529  dvmulbr  24530  dvferm1  24576  dvferm2  24578  ftc1lem6  24632  ig1peu  24759  ig1pdvds  24764  taylthlem1  24955  taylthlem2  24956  ulmdvlem3  24984  rlimcnp  25537  wilthlem2  25640  elpwdifcl  30281  iundisj2f  30334  ofpreima2  30405  iundisj2fi  30514  tocyccntz  30781  0nellinds  30930  lindsunlem  31015  lbsdiflsp0  31017  omsmeas  31576  eulerpartlemgs2  31633  ballotlemfrc  31779  hgt750lemd  31914  hgt750leme  31924  cvmscld  32515  unbdqndv1  33842  lindsadd  34879  lindsenlbs  34881  ftc1cnnc  34960  lsatfixedN  36139  dochsnkr  38602  hdmaprnlem4tN  38982  supminfxr2  41738  limcrecl  41903  cnrefiisplem  42103  fperdvper  42196  ismbl3  42265  ovolsplit  42267  ismbl4  42272  stoweidlem57  42336  dirkercncflem3  42384  fourierdlem42  42428  fourierdlem46  42431  fourierdlem62  42447  caragenuncllem  42788  caragendifcl  42790  omelesplit  42794  carageniuncllem2  42798  carageniuncl  42799  caragenel2d  42808  hspmbllem3  42904  hspmbl  42905  ovnsplit  42924  vonvolmbllem  42936  vonvolmbl  42937  c0rnghm  44178  lincdifsn  44473  lindslinindsimp1  44506  lincresunit3lem2  44529