Theorem ssdifssd 4110

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

Syntax hints:   → wi 4   ∖ cdif 3911   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-ss 3931

This theorem is referenced by:  xpord3pred  8131  unblem1  9239  fin23lem26  10278  fin23lem29  10294  isf32lem8  10313  fprodfvdvdsd  16304  mrieqvlemd  17590  mrieqv2d  17600  mrissmrid  17602  mreexmrid  17604  mreexexlem2d  17606  mreexexlem4d  17608  acsfiindd  18512  ablfac1eulem  20004  c0rnghm  20444  cntzsdrg  20711  lbspss  20989  lspsolv  21053  lsppratlem3  21059  lsppratlem4  21060  lspprat  21063  islbs2  21064  islbs3  21065  lbsextlem2  21069  lbsextlem3  21070  lbsextlem4  21071  lpss3  23031  islp3  23033  neitr  23067  restlp  23070  lpcls  23251  qtoprest  23604  ufinffr  23816  cldsubg  23998  xrge0gsumle  24722  bcthlem5  25228  rrxmval  25305  cmmbl  25435  nulmbl2  25437  shftmbl  25439  iundisj2  25450  uniiccdif  25479  uniiccmbl  25491  itg1val2  25585  itg1cl  25586  itg1ge0  25587  i1fadd  25596  itg1addlem5  25601  i1fmulc  25604  itg1mulc  25605  itg10a  25611  itg1ge0a  25612  itg1climres  25615  mbfi1fseqlem4  25619  itgss3  25716  limcdif  25777  limcnlp  25779  limcmpt2  25785  perfdvf  25804  dvcnp2  25821  dvcnp2OLD  25822  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvferm1  25889  dvferm2  25891  ftc1lem6  25948  ig1peu  26080  ig1pdvds  26085  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmdvlem3  26311  rlimcnp  26875  wilthlem2  26979  newf  27766  elpwdifcl  32455  iundisj2f  32519  ofpreima2  32590  iundisj2fi  32720  tocyccntz  33101  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  0nellinds  33341  elrspunidl  33399  rprmdvdsprod  33505  ig1pmindeg  33567  lindsunlem  33620  lbsdiflsp0  33622  dimlssid  33628  fldextrspunlsp  33669  omsmeas  34314  eulerpartlemgs2  34371  ballotlemfrc  34518  hgt750lemd  34639  hgt750leme  34649  cvmscld  35260  unbdqndv1  36496  lindsadd  37607  lindsenlbs  37609  ftc1cnnc  37686  lsatfixedN  39002  dochsnkr  41466  hdmaprnlem4tN  41846  redvmptabs  42348  prjcrv0  42621  supminfxr2  45465  limcrecl  45627  cnrefiisplem  45827  fperdvper  45917  ismbl3  45984  ovolsplit  45986  ismbl4  45991  stoweidlem57  46055  dirkercncflem3  46103  fourierdlem42  46147  fourierdlem46  46150  fourierdlem62  46166  caragenuncllem  46510  caragendifcl  46512  omelesplit  46516  carageniuncllem2  46520  carageniuncl  46521  caragenel2d  46530  hspmbllem3  46626  hspmbl  46627  ovnsplit  46646  vonvolmbllem  46658  vonvolmbl  46659  lincdifsn  48413  lindslinindsimp1  48446  lincresunit3lem2  48469