Theorem difssd 4068

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3885   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-dif 3891  df-in 3895  df-ss 3905

This theorem is referenced by:  uneqdifeq  4424  fpr1  8128  fofinf1o  9103  ackbij1lem12  9996  ssfin4  10075  enfin1ai  10149  fpwwe2  10408  wundif  10479  cshimadifsn  14551  fprodn0f  15710  rpnnen2lem11  15942  mrieqvlemd  17347  mrieqv2d  17357  symgextfo  19039  symgextres  19042  symgfixelsi  19052  pmtrdifellem1  19093  pmtrdifellem2  19094  dprdfeq0  19634  dpjf  19669  dpjlid  19673  dpjghm  19675  ablfac1eu  19685  subdrgint  20080  islbs3  20426  lbsextlem4  20432  frlmsslss2  20991  frlmlbs  21013  mdetrlin  21760  mdetrsca  21761  mdetralt  21766  mdetmul  21781  smadiadetlem3lem0  21823  smadiadet  21828  clsval2  22210  hausllycmp  22654  qtoprest  22877  trfil3  23048  ufileu  23079  fclscf  23185  alexsublem  23204  blcld  23670  restmetu  23735  evth  24131  lebnumlem1  24133  lebnumlem2  24134  lebnumlem3  24135  cmmbl  24707  nulmbl2  24709  volinun  24719  volsup  24729  uniioombllem3  24758  uniioombllem5  24760  uniioombl  24762  itg1addlem5  24874  itg2cnlem2  24936  dvreslem  25082  dvres2lem  25083  dvaddbr  25111  dvmulbr  25112  dvrec  25128  dvexp3  25151  dveflem  25152  dvcnvrelem2  25191  uhgrspan1  27679  unidifsnel  30892  fdifsuppconst  31032  fprodeq02  31146  gsumhashmul  31325  symgcom2  31362  cycpmconjvlem  31417  lindsunlem  31714  dimkerim  31717  madjusmdetlem1  31786  ist0cld  31792  indsum  31998  indsumin  31999  esumpad  32032  esumpad2  32033  measiun  32195  difelcarsg  32286  carsgclctunlem2  32295  tgoldbachgtde  32649  f1resrcmplf1d  33068  satfv1lem  33333  dmopab3rexdif  33376  mthmpps  33553  dvreasin  35872  dvreacos  35873  areacirclem4  35877  sticksstones22  40131  ntrclsrcomplex  41652  ntrclsfveq1  41677  ntrclsiso  41684  ntrclsk2  41685  ntrclskb  41686  ntrclsk3  41687  ntrclsk13  41688  ntrneircomplex  41691  clsneircomplex  41720  clsneiel1  41725  neicvgrcomplex  41730  neicvgel1  41736  difmap  42754  difmapsn  42759  supminfxr2  43016  iccdifprioo  43061  limciccioolb  43169  lptioo2  43179  lptioo1  43180  limcicciooub  43185  dvdivcncf  43475  itgvol0  43516  itgcoscmulx  43517  itgsincmulx  43522  ismbl3  43534  stoweidlem28  43576  stoweidlem50  43598  dirkeritg  43650  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem39  43694  fourierdlem58  43712  fourierdlem68  43722  fourierdlem76  43730  fourierdlem102  43756  fourierdlem114  43768  pwsal  43863  salexct  43880  sge0fodjrnlem  43961  iundjiun  44005  meaunle  44009  meadjiunlem  44010  meaiunlelem  44013  meadif  44024  meaiuninclem  44025  meaiininclem  44031  carageniuncllem2  44067  caragencmpl  44080  hsphoidmvle2  44130  hsphoidmvle  44131  hoidmv1lelem2  44137  hspmbllem1  44171  hspmbllem3  44173  fdmdifeqresdif  45688  lincdifsn  45776  lincresunit2  45830  lincresunit3lem2  45832  iscnrm3rlem3  46247  iscnrm3rlem7  46251