Theorem ssdifssd 4073

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

Syntax hints:   → wi 4   ∖ cdif 3880   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900

This theorem is referenced by:  unblem1  8996  fin23lem26  10012  fin23lem29  10028  isf32lem8  10047  fprodfvdvdsd  15971  mrieqvlemd  17255  mrieqv2d  17265  mrissmrid  17267  mreexmrid  17269  mreexexlem2d  17271  mreexexlem4d  17273  acsfiindd  18186  ablfac1eulem  19590  cntzsdrg  19985  lbspss  20259  lspsolv  20320  lsppratlem3  20326  lsppratlem4  20327  lspprat  20330  islbs2  20331  islbs3  20332  lbsextlem2  20336  lbsextlem3  20337  lbsextlem4  20338  lpss3  22203  islp3  22205  neitr  22239  restlp  22242  lpcls  22423  qtoprest  22776  ufinffr  22988  cldsubg  23170  xrge0gsumle  23902  bcthlem5  24397  rrxmval  24474  cmmbl  24603  nulmbl2  24605  shftmbl  24607  iundisj2  24618  uniiccdif  24647  uniiccmbl  24659  itg1val2  24753  itg1cl  24754  itg1ge0  24755  i1fadd  24764  itg1addlem5  24770  i1fmulc  24773  itg1mulc  24774  itg10a  24780  itg1ge0a  24781  itg1climres  24784  mbfi1fseqlem4  24788  itgss3  24884  limcdif  24945  limcnlp  24947  limcmpt2  24953  perfdvf  24972  dvcnp2  24989  dvaddbr  25007  dvmulbr  25008  dvferm1  25054  dvferm2  25056  ftc1lem6  25110  ig1peu  25241  ig1pdvds  25246  taylthlem1  25437  taylthlem2  25438  ulmdvlem3  25466  rlimcnp  26020  wilthlem2  26123  elpwdifcl  30776  iundisj2f  30830  ofpreima2  30905  iundisj2fi  31020  tocyccntz  31313  0nellinds  31468  elrspunidl  31508  lindsunlem  31607  lbsdiflsp0  31609  omsmeas  32190  eulerpartlemgs2  32247  ballotlemfrc  32393  hgt750lemd  32528  hgt750leme  32538  cvmscld  33135  xpord3pred  33725  newf  33969  unbdqndv1  34615  lindsadd  35697  lindsenlbs  35699  ftc1cnnc  35776  lsatfixedN  36950  dochsnkr  39413  hdmaprnlem4tN  39793  supminfxr2  42899  limcrecl  43060  cnrefiisplem  43260  fperdvper  43350  ismbl3  43417  ovolsplit  43419  ismbl4  43424  stoweidlem57  43488  dirkercncflem3  43536  fourierdlem42  43580  fourierdlem46  43583  fourierdlem62  43599  caragenuncllem  43940  caragendifcl  43942  omelesplit  43946  carageniuncllem2  43950  carageniuncl  43951  caragenel2d  43960  hspmbllem3  44056  hspmbl  44057  ovnsplit  44076  vonvolmbllem  44088  vonvolmbl  44089  c0rnghm  45359  lincdifsn  45653  lindslinindsimp1  45686  lincresunit3lem2  45709