Theorem difssd 4146

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3959   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-ss 3979

This theorem is referenced by:  uneqdifeq  4498  fpr1  8326  fofinf1o  9369  ackbij1lem12  10267  ssfin4  10347  enfin1ai  10421  fpwwe2  10680  wundif  10751  cshimadifsn  14864  fprodn0f  16023  rpnnen2lem11  16256  mrieqvlemd  17673  mrieqv2d  17683  symgextfo  19454  symgextres  19457  symgfixelsi  19467  pmtrdifellem1  19508  pmtrdifellem2  19509  dprdfeq0  20056  dpjf  20091  dpjlid  20095  dpjghm  20097  ablfac1eu  20107  subdrgint  20820  islbs3  21174  lbsextlem4  21180  cnflddiv  21430  frlmsslss2  21812  frlmlbs  21834  psdmul  22187  mdetrlin  22623  mdetrsca  22624  mdetralt  22629  mdetmul  22644  smadiadetlem3lem0  22686  smadiadet  22691  clsval2  23073  hausllycmp  23517  qtoprest  23740  trfil3  23911  ufileu  23942  fclscf  24048  alexsublem  24067  blcld  24533  restmetu  24598  evth  25004  lebnumlem1  25006  lebnumlem2  25007  lebnumlem3  25008  cmmbl  25582  nulmbl2  25584  volinun  25594  volsup  25604  uniioombllem3  25633  uniioombllem5  25635  uniioombl  25637  itg1addlem5  25749  itg2cnlem2  25811  dvreslem  25958  dvres2lem  25959  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvrec  26007  dvexp3  26030  dveflem  26031  dvcnvrelem2  26071  uhgrspan1  29334  unidifsnel  32560  fdifsupp  32699  fdifsuppconst  32703  fmptunsnop  32714  fprodeq02  32829  gsumhashmul  33046  symgcom2  33086  cycpmconjvlem  33143  domnprodn0  33261  rprmdvdsprod  33541  zringfrac  33561  lindsunlem  33651  dimkerim  33654  madjusmdetlem1  33787  ist0cld  33793  indsum  34001  indsumin  34002  esumpad  34035  esumpad2  34036  measiun  34198  difelcarsg  34291  carsgclctunlem2  34300  tgoldbachgtde  34653  f1resrcmplf1d  35079  satfv1lem  35346  dmopab3rexdif  35389  mthmpps  35566  dvreasin  37692  dvreacos  37693  areacirclem4  37697  sticksstones22  42149  selvvvval  42571  evlselvlem  42572  evlselv  42573  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  45149  difmapsn  45154  supminfxr2  45418  iccdifprioo  45468  limciccioolb  45576  lptioo2  45586  lptioo1  45587  limcicciooub  45592  dvdivcncf  45882  itgvol0  45923  itgcoscmulx  45924  itgsincmulx  45929  ismbl3  45941  stoweidlem28  45983  stoweidlem50  46005  dirkeritg  46057  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem39  46101  fourierdlem58  46119  fourierdlem68  46129  fourierdlem76  46137  fourierdlem102  46163  fourierdlem114  46175  pwsal  46270  salexct  46289  sge0fodjrnlem  46371  iundjiun  46415  meaunle  46419  meadjiunlem  46420  meaiunlelem  46423  meadif  46434  meaiuninclem  46435  meaiininclem  46441  carageniuncllem2  46477  caragencmpl  46490  hsphoidmvle2  46540  hsphoidmvle  46541  hoidmv1lelem2  46547  hspmbllem1  46581  hspmbllem3  46583  uhgrimisgrgric  47836  fdmdifeqresdif  48186  lincdifsn  48269  lincresunit2  48323  lincresunit3lem2  48325  iscnrm3rlem3  48738  iscnrm3rlem7  48742