Theorem difssd 4160

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

Assertion

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

Proof of Theorem difssd

Step	Hyp	Ref	Expression
1		difss 4159	. 2 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
2	1	a1i 11	1 ⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴)

Syntax hints:   → wi 4   ∖ cdif 3973   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-ss 3993

This theorem is referenced by:  uneqdifeq  4516  fpr1  8344  fofinf1o  9400  ackbij1lem12  10299  ssfin4  10379  enfin1ai  10453  fpwwe2  10712  wundif  10783  cshimadifsn  14878  fprodn0f  16039  rpnnen2lem11  16272  mrieqvlemd  17687  mrieqv2d  17697  symgextfo  19464  symgextres  19467  symgfixelsi  19477  pmtrdifellem1  19518  pmtrdifellem2  19519  dprdfeq0  20066  dpjf  20101  dpjlid  20105  dpjghm  20107  ablfac1eu  20117  subdrgint  20826  islbs3  21180  lbsextlem4  21186  cnflddiv  21436  frlmsslss2  21818  frlmlbs  21840  psdmul  22193  mdetrlin  22629  mdetrsca  22630  mdetralt  22635  mdetmul  22650  smadiadetlem3lem0  22692  smadiadet  22697  clsval2  23079  hausllycmp  23523  qtoprest  23746  trfil3  23917  ufileu  23948  fclscf  24054  alexsublem  24073  blcld  24539  restmetu  24604  evth  25010  lebnumlem1  25012  lebnumlem2  25013  lebnumlem3  25014  cmmbl  25588  nulmbl2  25590  volinun  25600  volsup  25610  uniioombllem3  25639  uniioombllem5  25641  uniioombl  25643  itg1addlem5  25755  itg2cnlem2  25817  dvreslem  25964  dvres2lem  25965  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvrec  26013  dvexp3  26036  dveflem  26037  dvcnvrelem2  26077  uhgrspan1  29338  unidifsnel  32563  fdifsuppconst  32701  fprodeq02  32827  gsumhashmul  33040  symgcom2  33077  cycpmconjvlem  33134  domnprodn0  33247  rprmdvdsprod  33527  zringfrac  33547  lindsunlem  33637  dimkerim  33640  madjusmdetlem1  33773  ist0cld  33779  indsum  33985  indsumin  33986  esumpad  34019  esumpad2  34020  measiun  34182  difelcarsg  34275  carsgclctunlem2  34284  tgoldbachgtde  34637  f1resrcmplf1d  35063  satfv1lem  35330  dmopab3rexdif  35373  mthmpps  35550  dvreasin  37666  dvreacos  37667  areacirclem4  37671  sticksstones22  42125  selvvvval  42540  evlselvlem  42541  evlselv  42542  ntrclsrcomplex  43997  ntrclsfveq1  44022  ntrclsiso  44029  ntrclsk2  44030  ntrclskb  44031  ntrclsk3  44032  ntrclsk13  44033  ntrneircomplex  44036  clsneircomplex  44065  clsneiel1  44070  neicvgrcomplex  44075  neicvgel1  44081  difmap  45114  difmapsn  45119  supminfxr2  45384  iccdifprioo  45434  limciccioolb  45542  lptioo2  45552  lptioo1  45553  limcicciooub  45558  dvdivcncf  45848  itgvol0  45889  itgcoscmulx  45890  itgsincmulx  45895  ismbl3  45907  stoweidlem28  45949  stoweidlem50  45971  dirkeritg  46023  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem39  46067  fourierdlem58  46085  fourierdlem68  46095  fourierdlem76  46103  fourierdlem102  46129  fourierdlem114  46141  pwsal  46236  salexct  46255  sge0fodjrnlem  46337  iundjiun  46381  meaunle  46385  meadjiunlem  46386  meaiunlelem  46389  meadif  46400  meaiuninclem  46401  meaiininclem  46407  carageniuncllem2  46443  caragencmpl  46456  hsphoidmvle2  46506  hsphoidmvle  46507  hoidmv1lelem2  46513  hspmbllem1  46547  hspmbllem3  46549  uhgrimisgrgric  47783  fdmdifeqresdif  48066  lincdifsn  48153  lincresunit2  48207  lincresunit3lem2  48209  iscnrm3rlem3  48622  iscnrm3rlem7  48626