Theorem difssd 4089

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3898   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-ss 3918

This theorem is referenced by:  uneqdifeq  4445  fpr1  8245  fofinf1o  9232  ackbij1lem12  10140  ssfin4  10220  enfin1ai  10294  fpwwe2  10554  wundif  10625  cshimadifsn  14752  fprodn0f  15914  rpnnen2lem11  16149  mrieqvlemd  17552  mrieqv2d  17562  symgextfo  19351  symgextres  19354  symgfixelsi  19364  pmtrdifellem1  19405  pmtrdifellem2  19406  dprdfeq0  19953  dpjf  19988  dpjlid  19992  dpjghm  19994  ablfac1eu  20004  subdrgint  20736  islbs3  21110  lbsextlem4  21116  cnflddiv  21355  frlmsslss2  21730  frlmlbs  21752  psdmul  22109  mdetrlin  22546  mdetrsca  22547  mdetralt  22552  mdetmul  22567  smadiadetlem3lem0  22609  smadiadet  22614  clsval2  22994  hausllycmp  23438  qtoprest  23661  trfil3  23832  ufileu  23863  fclscf  23969  alexsublem  23988  blcld  24449  restmetu  24514  evth  24914  lebnumlem1  24916  lebnumlem2  24917  lebnumlem3  24918  cmmbl  25491  nulmbl2  25493  volinun  25503  volsup  25513  uniioombllem3  25542  uniioombllem5  25544  uniioombl  25546  itg1addlem5  25657  itg2cnlem2  25719  dvreslem  25866  dvres2lem  25867  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvrec  25915  dvexp3  25938  dveflem  25939  dvcnvrelem2  25979  uhgrspan1  29376  unidifsnel  32610  fdifsupp  32764  fdifsuppconst  32768  fmptunsnop  32779  fprodeq02  32904  indsum  32942  indsumin  32943  gsumhashmul  33150  symgcom2  33166  cycpmconjvlem  33223  domnprodn0  33357  rprmdvdsprod  33615  zringfrac  33635  ply1coedeg  33670  extvfvvcl  33700  extvfvcl  33701  evlextv  33707  esplyind  33731  esplyindfv  33732  esplyfvn  33733  vieta  33736  lindsunlem  33781  dimkerim  33784  madjusmdetlem1  33984  ist0cld  33990  esumpad  34212  esumpad2  34213  measiun  34375  difelcarsg  34467  carsgclctunlem2  34476  tgoldbachgtde  34817  f1resrcmplf1d  35243  satfv1lem  35556  dmopab3rexdif  35599  mthmpps  35776  dvreasin  37907  dvreacos  37908  areacirclem4  37912  sticksstones22  42432  selvvvval  42838  evlselvlem  42839  evlselv  42840  ntrclsrcomplex  44286  ntrclsfveq1  44311  ntrclsiso  44318  ntrclsk2  44319  ntrclskb  44320  ntrclsk3  44321  ntrclsk13  44322  ntrneircomplex  44325  clsneircomplex  44354  clsneiel1  44359  neicvgrcomplex  44364  neicvgel1  44370  difmap  45461  difmapsn  45466  supminfxr2  45723  iccdifprioo  45772  limciccioolb  45877  lptioo2  45887  lptioo1  45888  limcicciooub  45891  dvdivcncf  46181  itgvol0  46222  itgcoscmulx  46223  itgsincmulx  46228  ismbl3  46240  stoweidlem28  46282  stoweidlem50  46304  dirkeritg  46356  dirkercncflem2  46358  dirkercncflem4  46360  fourierdlem39  46400  fourierdlem58  46418  fourierdlem68  46428  fourierdlem76  46436  fourierdlem102  46462  fourierdlem114  46474  pwsal  46569  salexct  46588  sge0fodjrnlem  46670  iundjiun  46714  meaunle  46718  meadjiunlem  46719  meaiunlelem  46722  meadif  46733  meaiuninclem  46734  meaiininclem  46740  carageniuncllem2  46776  caragencmpl  46789  hsphoidmvle2  46839  hsphoidmvle  46840  hoidmv1lelem2  46846  hspmbllem1  46880  hspmbllem3  46882  uhgrimisgrgric  48187  fdmdifeqresdif  48598  lincdifsn  48680  lincresunit2  48734  lincresunit3lem2  48736  iscnrm3rlem3  49197  iscnrm3rlem7  49201