Theorem difssd 4133

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3946   ⊆ wss 3949

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966

This theorem is referenced by:  uneqdifeq  4493  fpr1  8288  fofinf1o  9327  ackbij1lem12  10226  ssfin4  10305  enfin1ai  10379  fpwwe2  10638  wundif  10709  cshimadifsn  14780  fprodn0f  15935  rpnnen2lem11  16167  mrieqvlemd  17573  mrieqv2d  17583  symgextfo  19290  symgextres  19293  symgfixelsi  19303  pmtrdifellem1  19344  pmtrdifellem2  19345  dprdfeq0  19892  dpjf  19927  dpjlid  19931  dpjghm  19933  ablfac1eu  19943  subdrgint  20419  islbs3  20768  lbsextlem4  20774  frlmsslss2  21330  frlmlbs  21352  mdetrlin  22104  mdetrsca  22105  mdetralt  22110  mdetmul  22125  smadiadetlem3lem0  22167  smadiadet  22172  clsval2  22554  hausllycmp  22998  qtoprest  23221  trfil3  23392  ufileu  23423  fclscf  23529  alexsublem  23548  blcld  24014  restmetu  24079  evth  24475  lebnumlem1  24477  lebnumlem2  24478  lebnumlem3  24479  cmmbl  25051  nulmbl2  25053  volinun  25063  volsup  25073  uniioombllem3  25102  uniioombllem5  25104  uniioombl  25106  itg1addlem5  25218  itg2cnlem2  25280  dvreslem  25426  dvres2lem  25427  dvaddbr  25455  dvmulbr  25456  dvrec  25472  dvexp3  25495  dveflem  25496  dvcnvrelem2  25535  uhgrspan1  28560  unidifsnel  31772  fdifsuppconst  31911  fprodeq02  32029  gsumhashmul  32208  symgcom2  32245  cycpmconjvlem  32300  lindsunlem  32709  dimkerim  32712  madjusmdetlem1  32807  ist0cld  32813  indsum  33019  indsumin  33020  esumpad  33053  esumpad2  33054  measiun  33216  difelcarsg  33309  carsgclctunlem2  33318  tgoldbachgtde  33672  f1resrcmplf1d  34090  satfv1lem  34353  dmopab3rexdif  34396  mthmpps  34573  gg-dvmulbr  35175  dvreasin  36574  dvreacos  36575  areacirclem4  36579  sticksstones22  40984  selvvvval  41157  evlselvlem  41158  evlselv  41159  ntrclsrcomplex  42786  ntrclsfveq1  42811  ntrclsiso  42818  ntrclsk2  42819  ntrclskb  42820  ntrclsk3  42821  ntrclsk13  42822  ntrneircomplex  42825  clsneircomplex  42854  clsneiel1  42859  neicvgrcomplex  42864  neicvgel1  42870  difmap  43906  difmapsn  43911  supminfxr2  44179  iccdifprioo  44229  limciccioolb  44337  lptioo2  44347  lptioo1  44348  limcicciooub  44353  dvdivcncf  44643  itgvol0  44684  itgcoscmulx  44685  itgsincmulx  44690  ismbl3  44702  stoweidlem28  44744  stoweidlem50  44766  dirkeritg  44818  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem39  44862  fourierdlem58  44880  fourierdlem68  44890  fourierdlem76  44898  fourierdlem102  44924  fourierdlem114  44936  pwsal  45031  salexct  45050  sge0fodjrnlem  45132  iundjiun  45176  meaunle  45180  meadjiunlem  45181  meaiunlelem  45184  meadif  45195  meaiuninclem  45196  meaiininclem  45202  carageniuncllem2  45238  caragencmpl  45251  hsphoidmvle2  45301  hsphoidmvle  45302  hoidmv1lelem2  45308  hspmbllem1  45342  hspmbllem3  45344  fdmdifeqresdif  47017  lincdifsn  47105  lincresunit2  47159  lincresunit3lem2  47161  iscnrm3rlem3  47575  iscnrm3rlem7  47579