Theorem ssdifssd 4142

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

Syntax hints:   → wi 4   ∖ cdif 3945   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951  df-in 3955  df-ss 3965

This theorem is referenced by:  xpord3pred  8140  unblem1  9297  fin23lem26  10322  fin23lem29  10338  isf32lem8  10357  fprodfvdvdsd  16279  mrieqvlemd  17575  mrieqv2d  17585  mrissmrid  17587  mreexmrid  17589  mreexexlem2d  17591  mreexexlem4d  17593  acsfiindd  18508  ablfac1eulem  19944  cntzsdrg  20422  lbspss  20698  lspsolv  20762  lsppratlem3  20768  lsppratlem4  20769  lspprat  20772  islbs2  20773  islbs3  20774  lbsextlem2  20778  lbsextlem3  20779  lbsextlem4  20780  lpss3  22655  islp3  22657  neitr  22691  restlp  22694  lpcls  22875  qtoprest  23228  ufinffr  23440  cldsubg  23622  xrge0gsumle  24356  bcthlem5  24852  rrxmval  24929  cmmbl  25058  nulmbl2  25060  shftmbl  25062  iundisj2  25073  uniiccdif  25102  uniiccmbl  25114  itg1val2  25208  itg1cl  25209  itg1ge0  25210  i1fadd  25219  itg1addlem5  25225  i1fmulc  25228  itg1mulc  25229  itg10a  25235  itg1ge0a  25236  itg1climres  25239  mbfi1fseqlem4  25243  itgss3  25339  limcdif  25400  limcnlp  25402  limcmpt2  25408  perfdvf  25427  dvcnp2  25444  dvaddbr  25462  dvmulbr  25463  dvferm1  25509  dvferm2  25511  ftc1lem6  25565  ig1peu  25696  ig1pdvds  25701  taylthlem1  25892  taylthlem2  25893  ulmdvlem3  25921  rlimcnp  26477  wilthlem2  26580  newf  27361  elpwdifcl  31802  iundisj2f  31859  ofpreima2  31929  iundisj2fi  32046  tocyccntz  32344  0nellinds  32528  elrspunidl  32591  ig1pmindeg  32718  lindsunlem  32768  lbsdiflsp0  32770  omsmeas  33391  eulerpartlemgs2  33448  ballotlemfrc  33594  hgt750lemd  33729  hgt750leme  33739  cvmscld  34333  gg-dvcnp2  35243  gg-dvmulbr  35244  unbdqndv1  35470  lindsadd  36567  lindsenlbs  36569  ftc1cnnc  36646  lsatfixedN  37965  dochsnkr  40429  hdmaprnlem4tN  40809  prjcrv0  41457  supminfxr2  44258  limcrecl  44424  cnrefiisplem  44624  fperdvper  44714  ismbl3  44781  ovolsplit  44783  ismbl4  44788  stoweidlem57  44852  dirkercncflem3  44900  fourierdlem42  44944  fourierdlem46  44947  fourierdlem62  44963  caragenuncllem  45307  caragendifcl  45309  omelesplit  45313  carageniuncllem2  45317  carageniuncl  45318  caragenel2d  45327  hspmbllem3  45423  hspmbl  45424  ovnsplit  45443  vonvolmbllem  45455  vonvolmbl  45456  c0rnghm  46791  lincdifsn  47183  lindslinindsimp1  47216  lincresunit3lem2  47239