Theorem ssdifssd 4094

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

This proof depends on syntax axioms:   → wi 4   ∖ cdif 3896   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-ss 3916

This theorem is used by:  xpord3pred  8155  unblem1  9269  fin23lem26  10352  fin23lem29  10368  isf32lem8  10387  fprodfvdvdsd  16449  mrieqvlemd  17742  mrieqv2d  17752  mrissmrid  17754  mreexmrid  17756  mreexexlem2d  17758  mreexexlem4d  17760  acsfiindd  18666  ablfac1eulem  20227  c0rnghm  20726  cntzsdrg  20998  lbspss  21296  lspsolv  21360  lsppratlem3  21366  lsppratlem4  21367  lspprat  21370  islbs2  21371  islbs3  21372  lbsextlem2  21376  lbsextlem3  21377  lbsextlem4  21378  lindsenlbs  22096  lpss3  23401  islp3  23403  neitr  23437  restlp  23440  lpcls  23621  qtoprest  23975  ufinffr  24187  cldsubg  24369  xrge0gsumle  25092  bcthlem5  25588  rrxmval  25665  cmmbl  25794  nulmbl2  25796  shftmbl  25798  iundisj2  25809  uniiccdif  25838  uniiccmbl  25850  itg1val2  25944  itg1cl  25945  itg1ge0  25946  i1fadd  25955  itg1addlem5  25960  i1fmulc  25963  itg1mulc  25964  itg10a  25970  itg1ge0a  25971  itg1climres  25974  mbfi1fseqlem4  25978  itgss3  26074  limcdif  26135  limcnlp  26137  limcmpt2  26143  perfdvf  26162  dvcnp2  26179  dvaddbr  26197  dvmulbr  26198  dvferm1  26244  dvferm2  26246  ftc1lem6  26300  ig1peu  26432  ig1pdvds  26437  taylthlem1  26641  taylthlem2  26642  ulmdvlem3  26670  rlimcnp  27234  wilthlem2  27337  newf  28135  elpwdifcl  33033  iundisj2f  33095  ofpreima2  33171  iundisj2fi  33300  tocyccntz  33616  fxpsdrg  33647  elrgspnsubrunlem1  33719  elrgspnsubrunlem2  33720  0nellinds  33837  elrspunidl  33889  rprmdvdsprod  33977  ig1pmindeg  34045  lindsunlem  34167  lbsdiflsp0  34169  dimlssid  34175  fldextrspunlsp  34217  omsmeas  34867  eulerpartlemgs2  34924  ballotlemfrc  35071  hgt750lemd  35189  hgt750leme  35199  cvmscld  35935  unbdqndv1  37272  lindsadd  38432  ftc1cnnc  38506  lsatfixedN  39947  dochsnkr  42410  hdmaprnlem4tN  42790  redvmptabs  43300  prjcrv0  43544  supminfxr2  46362  limcrecl  46524  cnrefiisplem  46722  fperdvper  46812  ismbl3  46879  ovolsplit  46881  ismbl4  46886  stoweidlem57  46950  dirkercncflem3  46998  fourierdlem42  47042  fourierdlem46  47045  fourierdlem62  47061  caragenuncllem  47405  caragendifcl  47407  omelesplit  47411  carageniuncllem2  47415  carageniuncl  47416  caragenel2d  47425  hspmbllem3  47521  hspmbl  47522  ovnsplit  47541  vonvolmbllem  47553  vonvolmbl  47554  lincdifsn  49419  lindslinindsimp1  49452  lincresunit3lem2  49475