Theorem ssdifssd 4033

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

Syntax hints:   → wi 4   ∖ cdif 3840   ⊆ wss 3843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-dif 3846  df-in 3850  df-ss 3860

This theorem is referenced by:  unblem1  8844  fin23lem26  9825  fin23lem29  9841  isf32lem8  9860  fprodfvdvdsd  15779  mrieqvlemd  17003  mrieqv2d  17013  mrissmrid  17015  mreexmrid  17017  mreexexlem2d  17019  mreexexlem4d  17021  acsfiindd  17903  ablfac1eulem  19313  cntzsdrg  19700  lbspss  19973  lspsolv  20034  lsppratlem3  20040  lsppratlem4  20041  lspprat  20044  islbs2  20045  islbs3  20046  lbsextlem2  20050  lbsextlem3  20051  lbsextlem4  20052  lpss3  21895  islp3  21897  neitr  21931  restlp  21934  lpcls  22115  qtoprest  22468  ufinffr  22680  cldsubg  22862  xrge0gsumle  23585  bcthlem5  24080  rrxmval  24157  cmmbl  24286  nulmbl2  24288  shftmbl  24290  iundisj2  24301  uniiccdif  24330  uniiccmbl  24342  itg1val2  24436  itg1cl  24437  itg1ge0  24438  i1fadd  24447  itg1addlem5  24453  i1fmulc  24456  itg1mulc  24457  itg10a  24463  itg1ge0a  24464  itg1climres  24467  mbfi1fseqlem4  24471  itgss3  24567  limcdif  24628  limcnlp  24630  limcmpt2  24636  perfdvf  24655  dvcnp2  24672  dvaddbr  24690  dvmulbr  24691  dvferm1  24737  dvferm2  24739  ftc1lem6  24793  ig1peu  24924  ig1pdvds  24929  taylthlem1  25120  taylthlem2  25121  ulmdvlem3  25149  rlimcnp  25703  wilthlem2  25806  elpwdifcl  30449  iundisj2f  30503  ofpreima2  30578  iundisj2fi  30693  tocyccntz  30988  0nellinds  31138  elrspunidl  31178  lindsunlem  31277  lbsdiflsp0  31279  omsmeas  31860  eulerpartlemgs2  31917  ballotlemfrc  32063  hgt750lemd  32198  hgt750leme  32208  cvmscld  32806  xpord3pred  33409  newf  33683  unbdqndv1  34326  lindsadd  35393  lindsenlbs  35395  ftc1cnnc  35472  lsatfixedN  36646  dochsnkr  39109  hdmaprnlem4tN  39489  supminfxr2  42549  limcrecl  42712  cnrefiisplem  42912  fperdvper  43002  ismbl3  43069  ovolsplit  43071  ismbl4  43076  stoweidlem57  43140  dirkercncflem3  43188  fourierdlem42  43232  fourierdlem46  43235  fourierdlem62  43251  caragenuncllem  43592  caragendifcl  43594  omelesplit  43598  carageniuncllem2  43602  carageniuncl  43603  caragenel2d  43612  hspmbllem3  43708  hspmbl  43709  ovnsplit  43728  vonvolmbllem  43740  vonvolmbl  43741  c0rnghm  45005  lincdifsn  45299  lindslinindsimp1  45332  lincresunit3lem2  45355