Theorem difssd 4067

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3880   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-ss 3900

This theorem is referenced by:  uneqdifeq  4420  fpr1  8243  fofinf1o  9232  ackbij1lem12  10143  ssfin4  10223  enfin1ai  10297  fpwwe2  10557  wundif  10628  cshimadifsn  14782  indsum  15782  fprodn0f  15947  rpnnen2lem11  16182  mrieqvlemd  17586  mrieqv2d  17596  symgextfo  19388  symgextres  19391  symgfixelsi  19401  pmtrdifellem1  19442  pmtrdifellem2  19443  dprdfeq0  19990  dpjf  20025  dpjlid  20029  dpjghm  20031  ablfac1eu  20041  subdrgint  20775  islbs3  21148  lbsextlem4  21154  cnflddiv  21377  frlmsslss2  21750  frlmlbs  21772  selvvvval  22118  psdmul  22154  mdetrlin  22585  mdetrsca  22586  mdetralt  22591  mdetmul  22606  smadiadetlem3lem0  22648  smadiadet  22653  clsval2  23033  hausllycmp  23477  qtoprest  23700  trfil3  23871  ufileu  23902  fclscf  24008  alexsublem  24027  blcld  24488  restmetu  24553  evth  24944  lebnumlem1  24946  lebnumlem2  24947  lebnumlem3  24948  cmmbl  25519  nulmbl2  25521  volinun  25531  volsup  25541  uniioombllem3  25570  uniioombllem5  25572  uniioombl  25574  itg1addlem5  25685  itg2cnlem2  25747  dvreslem  25894  dvres2lem  25895  dvaddbr  25923  dvmulbr  25924  dvrec  25940  dvexp3  25963  dveflem  25964  dvcnvrelem2  26003  uhgrspan1  29390  unidifsnel  32623  fdifsupp  32777  fdifsuppconst  32781  fmptunsnop  32792  fprodeq02  32916  indsumin  32940  gsumhashmul  33148  suppgsumssiun  33153  symgcom2  33165  cycpmconjvlem  33222  domnprodn0  33356  rprmdvdsprod  33617  zringfrac  33637  ply1coedeg  33672  selvascl  33701  selvply1rhm0  33710  extvfvvcl  33719  extvfvcl  33720  evlextv  33726  psrmonprod  33736  esplyind  33759  esplyindfv  33760  esplyfvn  33761  vieta  33764  lindsunlem  33808  dimkerim  33811  madjusmdetlem1  34011  ist0cld  34017  esumpad  34239  esumpad2  34240  measiun  34402  difelcarsg  34494  carsgclctunlem2  34503  tgoldbachgtde  34844  f1resrcmplf1d  35268  satfv1lem  35590  dmopab3rexdif  35633  mthmpps  35810  dvreasin  38073  dvreacos  38074  areacirclem4  38078  sticksstones22  42653  evlselvlem  43038  evlselv  43039  ntrclsrcomplex  44479  ntrclsfveq1  44504  ntrclsiso  44511  ntrclsk2  44512  ntrclskb  44513  ntrclsk3  44514  ntrclsk13  44515  ntrneircomplex  44518  clsneircomplex  44547  clsneiel1  44552  neicvgrcomplex  44557  neicvgel1  44563  difmap  45652  difmapsn  45657  supminfxr2  45912  iccdifprioo  45961  limciccioolb  46066  lptioo2  46076  lptioo1  46077  limcicciooub  46080  dvdivcncf  46370  itgvol0  46411  itgcoscmulx  46412  itgsincmulx  46417  ismbl3  46429  stoweidlem28  46471  stoweidlem50  46493  dirkeritg  46545  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem39  46589  fourierdlem58  46607  fourierdlem68  46617  fourierdlem76  46625  fourierdlem102  46651  fourierdlem114  46663  pwsal  46758  salexct  46777  sge0fodjrnlem  46859  iundjiun  46903  meaunle  46907  meadjiunlem  46908  meaiunlelem  46911  meadif  46922  meaiuninclem  46923  meaiininclem  46929  carageniuncllem2  46965  caragencmpl  46978  hsphoidmvle2  47028  hsphoidmvle  47029  hoidmv1lelem2  47035  hspmbllem1  47069  hspmbllem3  47071  uhgrimisgrgric  48422  fdmdifeqresdif  48833  lincdifsn  48915  lincresunit2  48969  lincresunit3lem2  48971  iscnrm3rlem3  49432  iscnrm3rlem7  49436