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 ⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴)

Syntax hints:   → wi 4   ∖ cdif 3894   ⊆ wss 3897

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-ss 3914

This theorem is referenced by:  uneqdifeq  4440  fpr1  8233  fofinf1o  9216  ackbij1lem12  10121  ssfin4  10201  enfin1ai  10275  fpwwe2  10534  wundif  10605  cshimadifsn  14736  fprodn0f  15898  rpnnen2lem11  16133  mrieqvlemd  17535  mrieqv2d  17545  symgextfo  19334  symgextres  19337  symgfixelsi  19347  pmtrdifellem1  19388  pmtrdifellem2  19389  dprdfeq0  19936  dpjf  19971  dpjlid  19975  dpjghm  19977  ablfac1eu  19987  subdrgint  20718  islbs3  21092  lbsextlem4  21098  cnflddiv  21337  frlmsslss2  21712  frlmlbs  21734  psdmul  22081  mdetrlin  22517  mdetrsca  22518  mdetralt  22523  mdetmul  22538  smadiadetlem3lem0  22580  smadiadet  22585  clsval2  22965  hausllycmp  23409  qtoprest  23632  trfil3  23803  ufileu  23834  fclscf  23940  alexsublem  23959  blcld  24420  restmetu  24485  evth  24885  lebnumlem1  24887  lebnumlem2  24888  lebnumlem3  24889  cmmbl  25462  nulmbl2  25464  volinun  25474  volsup  25484  uniioombllem3  25513  uniioombllem5  25515  uniioombl  25517  itg1addlem5  25628  itg2cnlem2  25690  dvreslem  25837  dvres2lem  25838  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvrec  25886  dvexp3  25909  dveflem  25910  dvcnvrelem2  25950  uhgrspan1  29281  unidifsnel  32515  fdifsupp  32666  fdifsuppconst  32670  fmptunsnop  32681  fprodeq02  32806  indsum  32842  indsumin  32843  gsumhashmul  33041  symgcom2  33053  cycpmconjvlem  33110  domnprodn0  33242  rprmdvdsprod  33499  zringfrac  33519  lindsunlem  33637  dimkerim  33640  madjusmdetlem1  33840  ist0cld  33846  esumpad  34068  esumpad2  34069  measiun  34231  difelcarsg  34323  carsgclctunlem2  34332  tgoldbachgtde  34673  f1resrcmplf1d  35099  satfv1lem  35406  dmopab3rexdif  35449  mthmpps  35626  dvreasin  37756  dvreacos  37757  areacirclem4  37761  sticksstones22  42271  selvvvval  42688  evlselvlem  42689  evlselv  42690  ntrclsrcomplex  44138  ntrclsfveq1  44163  ntrclsiso  44170  ntrclsk2  44171  ntrclskb  44172  ntrclsk3  44173  ntrclsk13  44174  ntrneircomplex  44177  clsneircomplex  44206  clsneiel1  44211  neicvgrcomplex  44216  neicvgel1  44222  difmap  45314  difmapsn  45319  supminfxr2  45577  iccdifprioo  45626  limciccioolb  45731  lptioo2  45741  lptioo1  45742  limcicciooub  45745  dvdivcncf  46035  itgvol0  46076  itgcoscmulx  46077  itgsincmulx  46082  ismbl3  46094  stoweidlem28  46136  stoweidlem50  46158  dirkeritg  46210  dirkercncflem2  46212  dirkercncflem4  46214  fourierdlem39  46254  fourierdlem58  46272  fourierdlem68  46282  fourierdlem76  46290  fourierdlem102  46316  fourierdlem114  46328  pwsal  46423  salexct  46442  sge0fodjrnlem  46524  iundjiun  46568  meaunle  46572  meadjiunlem  46573  meaiunlelem  46576  meadif  46587  meaiuninclem  46588  meaiininclem  46594  carageniuncllem2  46630  caragencmpl  46643  hsphoidmvle2  46693  hsphoidmvle  46694  hoidmv1lelem2  46700  hspmbllem1  46734  hspmbllem3  46736  uhgrimisgrgric  48041  fdmdifeqresdif  48452  lincdifsn  48535  lincresunit2  48589  lincresunit3lem2  48591  iscnrm3rlem3  49052  iscnrm3rlem7  49056