Theorem difssd 4063

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3880   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900

This theorem is referenced by:  uneqdifeq  4420  fpr1  8090  fofinf1o  9024  ackbij1lem12  9918  ssfin4  9997  enfin1ai  10071  fpwwe2  10330  wundif  10401  cshimadifsn  14470  fprodn0f  15629  rpnnen2lem11  15861  mrieqvlemd  17255  mrieqv2d  17265  symgextfo  18945  symgextres  18948  symgfixelsi  18958  pmtrdifellem1  18999  pmtrdifellem2  19000  dprdfeq0  19540  dpjf  19575  dpjlid  19579  dpjghm  19581  ablfac1eu  19591  subdrgint  19986  islbs3  20332  lbsextlem4  20338  frlmsslss2  20892  frlmlbs  20914  mdetrlin  21659  mdetrsca  21660  mdetralt  21665  mdetmul  21680  smadiadetlem3lem0  21722  smadiadet  21727  clsval2  22109  hausllycmp  22553  qtoprest  22776  trfil3  22947  ufileu  22978  fclscf  23084  alexsublem  23103  blcld  23567  restmetu  23632  evth  24028  lebnumlem1  24030  lebnumlem2  24031  lebnumlem3  24032  cmmbl  24603  nulmbl2  24605  volinun  24615  volsup  24625  uniioombllem3  24654  uniioombllem5  24656  uniioombl  24658  itg1addlem5  24770  itg2cnlem2  24832  dvreslem  24978  dvres2lem  24979  dvaddbr  25007  dvmulbr  25008  dvrec  25024  dvexp3  25047  dveflem  25048  dvcnvrelem2  25087  uhgrspan1  27573  unidifsnel  30784  fdifsuppconst  30925  fprodeq02  31039  gsumhashmul  31218  symgcom2  31255  cycpmconjvlem  31310  lindsunlem  31607  dimkerim  31610  madjusmdetlem1  31679  ist0cld  31685  indsum  31889  indsumin  31890  esumpad  31923  esumpad2  31924  measiun  32086  difelcarsg  32177  carsgclctunlem2  32186  tgoldbachgtde  32540  f1resrcmplf1d  32959  satfv1lem  33224  dmopab3rexdif  33267  mthmpps  33444  dvreasin  35790  dvreacos  35791  areacirclem4  35795  sticksstones22  40052  ntrclsrcomplex  41534  ntrclsfveq1  41559  ntrclsiso  41566  ntrclsk2  41567  ntrclskb  41568  ntrclsk3  41569  ntrclsk13  41570  ntrneircomplex  41573  clsneircomplex  41602  clsneiel1  41607  neicvgrcomplex  41612  neicvgel1  41618  difmap  42636  difmapsn  42641  supminfxr2  42899  iccdifprioo  42944  limciccioolb  43052  lptioo2  43062  lptioo1  43063  limcicciooub  43068  dvdivcncf  43358  itgvol0  43399  itgcoscmulx  43400  itgsincmulx  43405  ismbl3  43417  stoweidlem28  43459  stoweidlem50  43481  dirkeritg  43533  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem39  43577  fourierdlem58  43595  fourierdlem68  43605  fourierdlem76  43613  fourierdlem102  43639  fourierdlem114  43651  pwsal  43746  salexct  43763  sge0fodjrnlem  43844  iundjiun  43888  meaunle  43892  meadjiunlem  43893  meaiunlelem  43896  meadif  43907  meaiuninclem  43908  meaiininclem  43914  carageniuncllem2  43950  caragencmpl  43963  hsphoidmvle2  44013  hsphoidmvle  44014  hoidmv1lelem2  44020  hspmbllem1  44054  hspmbllem3  44056  fdmdifeqresdif  45565  lincdifsn  45653  lincresunit2  45707  lincresunit3lem2  45709  iscnrm3rlem3  46124  iscnrm3rlem7  46128