Theorem difssd 4109

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3933   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-in 3943  df-ss 3952

This theorem is referenced by:  uneqdifeq  4438  fofinf1o  8799  ackbij1lem12  9653  ssfin4  9732  enfin1ai  9806  fpwwe2  10065  wundif  10136  cshimadifsn  14191  fprodn0f  15345  rpnnen2lem11  15577  mrieqvlemd  16900  mrieqv2d  16910  symgextfo  18550  symgextres  18553  symgfixelsi  18563  pmtrdifellem1  18604  pmtrdifellem2  18605  dprdfeq0  19144  dpjf  19179  dpjlid  19183  dpjghm  19185  ablfac1eu  19195  subdrgint  19582  islbs3  19927  lbsextlem4  19933  frlmsslss2  20919  frlmlbs  20941  mdetrlin  21211  mdetrsca  21212  mdetralt  21217  mdetmul  21232  smadiadetlem3lem0  21274  smadiadet  21279  clsval2  21658  hausllycmp  22102  qtoprest  22325  trfil3  22496  ufileu  22527  fclscf  22633  alexsublem  22652  blcld  23115  restmetu  23180  evth  23563  lebnumlem1  23565  lebnumlem2  23566  lebnumlem3  23567  cmmbl  24135  nulmbl2  24137  volinun  24147  volsup  24157  uniioombllem3  24186  uniioombllem5  24188  uniioombl  24190  itg1addlem5  24301  itg2cnlem2  24363  dvreslem  24507  dvres2lem  24508  dvaddbr  24535  dvmulbr  24536  dvrec  24552  dvexp3  24575  dveflem  24576  dvcnvrelem2  24615  uhgrspan1  27085  unidifsnel  30295  fprodeq02  30539  symgcom2  30728  cycpmconjvlem  30783  lindsunlem  31020  dimkerim  31023  madjusmdetlem1  31092  indsum  31280  indsumin  31281  esumpad  31314  esumpad2  31315  measiun  31477  difelcarsg  31568  carsgclctunlem2  31577  tgoldbachgtde  31931  f1resrcmplf1d  32360  satfv1lem  32609  dmopab3rexdif  32652  mthmpps  32829  fpr1  33139  dvreasin  34995  dvreacos  34996  areacirclem4  35000  ntrclsrcomplex  40405  ntrclsfveq1  40430  ntrclsiso  40437  ntrclsk2  40438  ntrclskb  40439  ntrclsk3  40440  ntrclsk13  40441  ntrneircomplex  40444  clsneircomplex  40473  clsneiel1  40478  neicvgrcomplex  40483  neicvgel1  40489  difmap  41490  difmapsn  41495  supminfxr2  41765  iccdifprioo  41812  limciccioolb  41922  lptioo2  41932  lptioo1  41933  limcicciooub  41938  dvdivcncf  42232  itgvol0  42273  itgcoscmulx  42274  itgsincmulx  42279  ismbl3  42291  stoweidlem28  42333  stoweidlem50  42355  dirkeritg  42407  dirkercncflem2  42409  dirkercncflem4  42411  fourierdlem39  42451  fourierdlem58  42469  fourierdlem68  42479  fourierdlem76  42487  fourierdlem102  42513  fourierdlem114  42525  pwsal  42620  salexct  42637  sge0fodjrnlem  42718  iundjiun  42762  meaunle  42766  meadjiunlem  42767  meaiunlelem  42770  meadif  42781  meaiuninclem  42782  meaiininclem  42788  carageniuncllem2  42824  caragencmpl  42837  hsphoidmvle2  42887  hsphoidmvle  42888  hoidmv1lelem2  42894  hspmbllem1  42928  hspmbllem3  42930  fdmdifeqresdif  44410  lincdifsn  44499  lincresunit2  44553  lincresunit3lem2  44555