Theorem difssd 4100

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3911   ⊆ wss 3914

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 3449  df-dif 3917  df-ss 3931

This theorem is referenced by:  uneqdifeq  4456  fpr1  8282  fofinf1o  9283  ackbij1lem12  10183  ssfin4  10263  enfin1ai  10337  fpwwe2  10596  wundif  10667  cshimadifsn  14795  fprodn0f  15957  rpnnen2lem11  16192  mrieqvlemd  17590  mrieqv2d  17600  symgextfo  19352  symgextres  19355  symgfixelsi  19365  pmtrdifellem1  19406  pmtrdifellem2  19407  dprdfeq0  19954  dpjf  19989  dpjlid  19993  dpjghm  19995  ablfac1eu  20005  subdrgint  20712  islbs3  21065  lbsextlem4  21071  cnflddiv  21312  frlmsslss2  21684  frlmlbs  21706  psdmul  22053  mdetrlin  22489  mdetrsca  22490  mdetralt  22495  mdetmul  22510  smadiadetlem3lem0  22552  smadiadet  22557  clsval2  22937  hausllycmp  23381  qtoprest  23604  trfil3  23775  ufileu  23806  fclscf  23912  alexsublem  23931  blcld  24393  restmetu  24458  evth  24858  lebnumlem1  24860  lebnumlem2  24861  lebnumlem3  24862  cmmbl  25435  nulmbl2  25437  volinun  25447  volsup  25457  uniioombllem3  25486  uniioombllem5  25488  uniioombl  25490  itg1addlem5  25601  itg2cnlem2  25663  dvreslem  25810  dvres2lem  25811  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvrec  25859  dvexp3  25882  dveflem  25883  dvcnvrelem2  25923  uhgrspan1  29230  unidifsnel  32464  fdifsupp  32608  fdifsuppconst  32612  fmptunsnop  32623  fprodeq02  32748  indsum  32784  indsumin  32785  gsumhashmul  33001  symgcom2  33041  cycpmconjvlem  33098  domnprodn0  33226  rprmdvdsprod  33505  zringfrac  33525  lindsunlem  33620  dimkerim  33623  madjusmdetlem1  33817  ist0cld  33823  esumpad  34045  esumpad2  34046  measiun  34208  difelcarsg  34301  carsgclctunlem2  34310  tgoldbachgtde  34651  f1resrcmplf1d  35077  satfv1lem  35349  dmopab3rexdif  35392  mthmpps  35569  dvreasin  37700  dvreacos  37701  areacirclem4  37705  sticksstones22  42156  selvvvval  42573  evlselvlem  42574  evlselv  42575  ntrclsrcomplex  44024  ntrclsfveq1  44049  ntrclsiso  44056  ntrclsk2  44057  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  ntrneircomplex  44063  clsneircomplex  44092  clsneiel1  44097  neicvgrcomplex  44102  neicvgel1  44108  difmap  45201  difmapsn  45206  supminfxr2  45465  iccdifprioo  45514  limciccioolb  45619  lptioo2  45629  lptioo1  45630  limcicciooub  45635  dvdivcncf  45925  itgvol0  45966  itgcoscmulx  45967  itgsincmulx  45972  ismbl3  45984  stoweidlem28  46026  stoweidlem50  46048  dirkeritg  46100  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem39  46144  fourierdlem58  46162  fourierdlem68  46172  fourierdlem76  46180  fourierdlem102  46206  fourierdlem114  46218  pwsal  46313  salexct  46332  sge0fodjrnlem  46414  iundjiun  46458  meaunle  46462  meadjiunlem  46463  meaiunlelem  46466  meadif  46477  meaiuninclem  46478  meaiininclem  46484  carageniuncllem2  46520  caragencmpl  46533  hsphoidmvle2  46583  hsphoidmvle  46584  hoidmv1lelem2  46590  hspmbllem1  46624  hspmbllem3  46626  uhgrimisgrgric  47931  fdmdifeqresdif  48330  lincdifsn  48413  lincresunit2  48467  lincresunit3lem2  48469  iscnrm3rlem3  48930  iscnrm3rlem7  48934