Theorem difssd 4088

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3900   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906  df-ss 3920

This theorem is referenced by:  uneqdifeq  4444  fpr1  8236  fofinf1o  9222  ackbij1lem12  10124  ssfin4  10204  enfin1ai  10278  fpwwe2  10537  wundif  10608  cshimadifsn  14736  fprodn0f  15898  rpnnen2lem11  16133  mrieqvlemd  17535  mrieqv2d  17545  symgextfo  19301  symgextres  19304  symgfixelsi  19314  pmtrdifellem1  19355  pmtrdifellem2  19356  dprdfeq0  19903  dpjf  19938  dpjlid  19942  dpjghm  19944  ablfac1eu  19954  subdrgint  20688  islbs3  21062  lbsextlem4  21068  cnflddiv  21307  frlmsslss2  21682  frlmlbs  21704  psdmul  22051  mdetrlin  22487  mdetrsca  22488  mdetralt  22493  mdetmul  22508  smadiadetlem3lem0  22550  smadiadet  22555  clsval2  22935  hausllycmp  23379  qtoprest  23602  trfil3  23773  ufileu  23804  fclscf  23910  alexsublem  23929  blcld  24391  restmetu  24456  evth  24856  lebnumlem1  24858  lebnumlem2  24859  lebnumlem3  24860  cmmbl  25433  nulmbl2  25435  volinun  25445  volsup  25455  uniioombllem3  25484  uniioombllem5  25486  uniioombl  25488  itg1addlem5  25599  itg2cnlem2  25661  dvreslem  25808  dvres2lem  25809  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  dvrec  25857  dvexp3  25880  dveflem  25881  dvcnvrelem2  25921  uhgrspan1  29248  unidifsnel  32479  fdifsupp  32627  fdifsuppconst  32631  fmptunsnop  32642  fprodeq02  32768  indsum  32804  indsumin  32805  gsumhashmul  33014  symgcom2  33026  cycpmconjvlem  33083  domnprodn0  33215  rprmdvdsprod  33471  zringfrac  33491  lindsunlem  33591  dimkerim  33594  madjusmdetlem1  33794  ist0cld  33800  esumpad  34022  esumpad2  34023  measiun  34185  difelcarsg  34278  carsgclctunlem2  34287  tgoldbachgtde  34628  f1resrcmplf1d  35054  satfv1lem  35339  dmopab3rexdif  35382  mthmpps  35559  dvreasin  37690  dvreacos  37691  areacirclem4  37695  sticksstones22  42145  selvvvval  42562  evlselvlem  42563  evlselv  42564  ntrclsrcomplex  44012  ntrclsfveq1  44037  ntrclsiso  44044  ntrclsk2  44045  ntrclskb  44046  ntrclsk3  44047  ntrclsk13  44048  ntrneircomplex  44051  clsneircomplex  44080  clsneiel1  44085  neicvgrcomplex  44090  neicvgel1  44096  difmap  45189  difmapsn  45194  supminfxr2  45452  iccdifprioo  45501  limciccioolb  45606  lptioo2  45616  lptioo1  45617  limcicciooub  45622  dvdivcncf  45912  itgvol0  45953  itgcoscmulx  45954  itgsincmulx  45959  ismbl3  45971  stoweidlem28  46013  stoweidlem50  46035  dirkeritg  46087  dirkercncflem2  46089  dirkercncflem4  46091  fourierdlem39  46131  fourierdlem58  46149  fourierdlem68  46159  fourierdlem76  46167  fourierdlem102  46193  fourierdlem114  46205  pwsal  46300  salexct  46319  sge0fodjrnlem  46401  iundjiun  46445  meaunle  46449  meadjiunlem  46450  meaiunlelem  46453  meadif  46464  meaiuninclem  46465  meaiininclem  46471  carageniuncllem2  46507  caragencmpl  46520  hsphoidmvle2  46570  hsphoidmvle  46571  hoidmv1lelem2  46577  hspmbllem1  46611  hspmbllem3  46613  uhgrimisgrgric  47919  fdmdifeqresdif  48330  lincdifsn  48413  lincresunit2  48467  lincresunit3lem2  48469  iscnrm3rlem3  48930  iscnrm3rlem7  48934