Theorem difssd 4090

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

Assertion

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

Proof of Theorem difssd

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-dif 3907  df-ss 3921

This theorem is referenced by:  uneqdifeq  4446  fpr1  8284  fofinf1o  9275  ackbij1lem12  10186  ssfin4  10267  enfin1ai  10341  fpwwe2  10601  wundif  10672  cshimadifsn  14842  indsum  15856  fprodn0f  16021  rpnnen2lem11  16256  mrieqvlemd  17661  mrieqv2d  17671  symgextfo  19462  symgextres  19465  symgfixelsi  19475  pmtrdifellem1  19516  pmtrdifellem2  19517  dprdfeq0  20064  dpjf  20099  dpjlid  20103  dpjghm  20105  ablfac1eu  20115  subdrgint  20852  islbs3  21225  lbsextlem4  21231  cnflddiv  21454  frlmsslss2  21827  frlmlbs  21849  selvvvval  22195  psdmul  22231  mdetrlin  22662  mdetrsca  22663  mdetralt  22668  mdetmul  22683  smadiadetlem3lem0  22725  smadiadet  22730  clsval2  23110  hausllycmp  23554  qtoprest  23777  trfil3  23948  ufileu  23979  fclscf  24085  alexsublem  24104  blcld  24565  restmetu  24630  evth  25021  lebnumlem1  25023  lebnumlem2  25024  lebnumlem3  25025  cmmbl  25596  nulmbl2  25598  volinun  25608  volsup  25618  uniioombllem3  25647  uniioombllem5  25649  uniioombl  25651  itg1addlem5  25762  itg2cnlem2  25824  dvreslem  25971  dvres2lem  25972  dvaddbr  26000  dvmulbr  26001  dvrec  26017  dvexp3  26040  dveflem  26041  dvcnvrelem2  26080  uhgrspan1  29504  unidifsnel  32734  fdifsupp  32887  fdifsuppconst  32891  fmptunsnop  32902  fprodeq02  33026  indsumin  33039  gsumhashmul  33247  suppgsumssiun  33252  symgcom2  33264  cycpmconjvlem  33321  domnprodn0  33459  dflringlem2  33691  rprmdvdsprod  33730  zringfrac  33750  ply1coedeg  33785  selvascl  33814  selvply1rhm0  33823  extvfvvcl  33832  extvfvcl  33833  evlextv  33839  psrmonprod  33849  esplyind  33872  esplyindfv  33873  esplyfvn  33874  vieta  33877  lindsunlem  33921  dimkerim  33924  madjusmdetlem1  34124  ist0cld  34130  esumpad  34352  esumpad2  34353  measiun  34515  difelcarsg  34607  carsgclctunlem2  34616  tgoldbachgtde  34954  f1resrcmplf1d  35381  satfv1lem  35712  dmopab3rexdif  35755  mthmpps  35932  dvreasin  38205  dvreacos  38206  areacirclem4  38210  sticksstones22  42785  evlselvlem  43170  evlselv  43171  ntrclsrcomplex  44611  ntrclsfveq1  44636  ntrclsiso  44643  ntrclsk2  44644  ntrclskb  44645  ntrclsk3  44646  ntrclsk13  44647  ntrneircomplex  44650  clsneircomplex  44679  clsneiel1  44684  neicvgrcomplex  44689  neicvgel1  44695  difmap  45783  difmapsn  45788  supminfxr2  46043  iccdifprioo  46092  limciccioolb  46197  lptioo2  46207  lptioo1  46208  limcicciooub  46211  dvdivcncf  46501  itgvol0  46542  itgcoscmulx  46543  itgsincmulx  46548  ismbl3  46560  stoweidlem28  46602  stoweidlem50  46624  dirkeritg  46676  dirkercncflem2  46678  dirkercncflem4  46680  fourierdlem39  46720  fourierdlem58  46738  fourierdlem68  46748  fourierdlem76  46756  fourierdlem102  46782  fourierdlem114  46794  pwsal  46889  salexct  46908  sge0fodjrnlem  46990  iundjiun  47034  meaunle  47038  meadjiunlem  47039  meaiunlelem  47042  meadif  47053  meaiuninclem  47054  meaiininclem  47060  carageniuncllem2  47096  caragencmpl  47109  hsphoidmvle2  47159  hsphoidmvle  47160  hoidmv1lelem2  47166  hspmbllem1  47200  hspmbllem3  47202  uhgrimisgrgric  48553  fdmdifeqresdif  48964  lincdifsn  49046  lincresunit2  49100  lincresunit3lem2  49102  iscnrm3rlem3  49563  iscnrm3rlem7  49567