Theorem difssd 4084

Description: A difference of two classes is contained in the minuend. Deduction form of difss 4083. (Contributed by David Moews, 1-May-2017.)

Assertion

Ref	Expression
difssd	⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴)

Proof of Theorem difssd

Step	Hyp	Ref	Expression
1		difss 4083	. 2 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
2	1	a1i 11	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:  uneqdifeq  4448  f1resrcmplf1d  7273  fpr1  8303  fofinf1o  9300  ackbij1lem12  10233  ssfin4  10313  enfin1ai  10387  fpwwe2  10653  wundif  10724  cshimadifsn  14901  indsum  15916  fprodn0f  16079  rpnnen2lem11  16313  mrieqvlemd  17718  mrieqv2d  17728  symgextfo  19550  symgextres  19553  symgfixelsi  19563  pmtrdifellem1  19604  pmtrdifellem2  19605  dprdfeq0  20152  dpjf  20187  dpjlid  20191  dpjghm  20193  ablfac1eu  20203  isdrng3lem1  20915  subdrgint  20970  islbs3  21343  lbsextlem4  21349  cnflddiv  21616  frlmsslss2  21989  frlmlbs  22011  selvvvval  22359  psdmul  22395  mdetrlin  22825  mdetrsca  22826  mdetralt  22831  mdetmul  22846  smadiadetlem3lem0  22888  smadiadet  22893  clsval2  23276  hausllycmp  23721  qtoprest  23944  trfil3  24115  ufileu  24146  fclscf  24252  alexsublem  24271  blcld  24732  restmetu  24797  evth  25188  lebnumlem1  25190  lebnumlem2  25191  lebnumlem3  25192  cmmbl  25763  nulmbl2  25765  volinun  25775  volsup  25785  uniioombllem3  25814  uniioombllem5  25816  uniioombl  25818  itg1addlem5  25929  itg2cnlem2  25991  dvreslem  26137  dvres2lem  26138  dvaddbr  26166  dvmulbr  26167  dvrec  26183  dvexp3  26206  dveflem  26207  dvcnvrelem2  26246  uhgrspan1  29764  unidifsnel  33011  fdifsupp  33158  fdifsuppconst  33162  fmptunsnop  33173  fprodeq02  33295  indsumin  33308  gsumhashmul  33508  suppgsumssiun  33513  symgcom2  33525  cycpmconjvlem  33582  domnprodn0  33719  dflringlem2  33906  rprmdvdsprod  33945  zringfrac  33965  ply1coedeg  34000  selvascl  34028  selvply1rhm0  34037  extvfvvcl  34046  extvfvcl  34047  evlextv  34053  psrmonprod  34063  esplyind  34086  esplyindfv  34087  esplyfvn  34088  vieta  34091  lindsunlem  34135  dimkerim  34138  madjusmdetlem1  34338  ist0cld  34344  esumpad  34566  esumpad2  34567  measiun  34730  difelcarsg  34822  carsgclctunlem2  34831  tgoldbachgtde  35169  satfv1lem  35942  dmopab3rexdif  35985  mthmpps  36162  dvreasin  38456  dvreacos  38457  areacirclem4  38461  sticksstones22  43035  evlselvlem  43435  evlselv  43436  ntrclsrcomplex  44876  ntrclsfveq1  44901  ntrclsiso  44908  ntrclsk2  44909  ntrclskb  44910  ntrclsk3  44911  ntrclsk13  44912  ntrneircomplex  44915  clsneircomplex  44944  clsneiel1  44949  neicvgrcomplex  44954  neicvgel1  44960  difmap  46038  difmapsn  46043  supminfxr2  46298  iccdifprioo  46347  limciccioolb  46452  lptioo2  46462  lptioo1  46463  limcicciooub  46466  dvdivcncf  46756  itgvol0  46797  itgcoscmulx  46798  itgsincmulx  46803  ismbl3  46815  stoweidlem28  46857  stoweidlem50  46879  dirkeritg  46931  dirkercncflem2  46933  dirkercncflem4  46935  fourierdlem39  46975  fourierdlem58  46993  fourierdlem68  47003  fourierdlem76  47011  fourierdlem102  47037  fourierdlem114  47049  pwsal  47144  salexct  47163  sge0fodjrnlem  47245  iundjiun  47289  meaunle  47293  meadjiunlem  47294  meaiunlelem  47297  meadif  47308  meaiuninclem  47309  meaiininclem  47315  carageniuncllem2  47351  caragencmpl  47364  hsphoidmvle2  47414  hsphoidmvle  47415  hoidmv1lelem2  47421  hspmbllem1  47455  hspmbllem3  47457  uhgrimisgrgric  48848  fdmdifeqresdif  49273  lincdifsn  49355  lincresunit2  49409  lincresunit3lem2  49411  iscnrm3rlem3  49869  iscnrm3rlem7  49873