Theorem difssd 4089

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3898   ⊆ wss 3901

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-ss 3918

This theorem is referenced by:  uneqdifeq  4445  fpr1  8245  fofinf1o  9232  ackbij1lem12  10140  ssfin4  10220  enfin1ai  10294  fpwwe2  10554  wundif  10625  cshimadifsn  14752  fprodn0f  15914  rpnnen2lem11  16149  mrieqvlemd  17552  mrieqv2d  17562  symgextfo  19351  symgextres  19354  symgfixelsi  19364  pmtrdifellem1  19405  pmtrdifellem2  19406  dprdfeq0  19953  dpjf  19988  dpjlid  19992  dpjghm  19994  ablfac1eu  20004  subdrgint  20736  islbs3  21110  lbsextlem4  21116  cnflddiv  21355  frlmsslss2  21730  frlmlbs  21752  psdmul  22109  mdetrlin  22546  mdetrsca  22547  mdetralt  22552  mdetmul  22567  smadiadetlem3lem0  22609  smadiadet  22614  clsval2  22994  hausllycmp  23438  qtoprest  23661  trfil3  23832  ufileu  23863  fclscf  23969  alexsublem  23988  blcld  24449  restmetu  24514  evth  24914  lebnumlem1  24916  lebnumlem2  24917  lebnumlem3  24918  cmmbl  25491  nulmbl2  25493  volinun  25503  volsup  25513  uniioombllem3  25542  uniioombllem5  25544  uniioombl  25546  itg1addlem5  25657  itg2cnlem2  25719  dvreslem  25866  dvres2lem  25867  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvrec  25915  dvexp3  25938  dveflem  25939  dvcnvrelem2  25979  uhgrspan1  29376  unidifsnel  32610  fdifsupp  32764  fdifsuppconst  32768  fmptunsnop  32779  fprodeq02  32904  indsum  32942  indsumin  32943  gsumhashmul  33150  symgcom2  33166  cycpmconjvlem  33223  domnprodn0  33357  rprmdvdsprod  33615  zringfrac  33635  ply1coedeg  33670  extvfvvcl  33700  extvfvcl  33701  evlextv  33707  esplyind  33731  esplyindfv  33732  esplyfvn  33733  vieta  33736  lindsunlem  33781  dimkerim  33784  madjusmdetlem1  33984  ist0cld  33990  esumpad  34212  esumpad2  34213  measiun  34375  difelcarsg  34467  carsgclctunlem2  34476  tgoldbachgtde  34817  f1resrcmplf1d  35243  satfv1lem  35556  dmopab3rexdif  35599  mthmpps  35776  dvreasin  37903  dvreacos  37904  areacirclem4  37908  sticksstones22  42418  selvvvval  42824  evlselvlem  42825  evlselv  42826  ntrclsrcomplex  44272  ntrclsfveq1  44297  ntrclsiso  44304  ntrclsk2  44305  ntrclskb  44306  ntrclsk3  44307  ntrclsk13  44308  ntrneircomplex  44311  clsneircomplex  44340  clsneiel1  44345  neicvgrcomplex  44350  neicvgel1  44356  difmap  45447  difmapsn  45452  supminfxr2  45709  iccdifprioo  45758  limciccioolb  45863  lptioo2  45873  lptioo1  45874  limcicciooub  45877  dvdivcncf  46167  itgvol0  46208  itgcoscmulx  46209  itgsincmulx  46214  ismbl3  46226  stoweidlem28  46268  stoweidlem50  46290  dirkeritg  46342  dirkercncflem2  46344  dirkercncflem4  46346  fourierdlem39  46386  fourierdlem58  46404  fourierdlem68  46414  fourierdlem76  46422  fourierdlem102  46448  fourierdlem114  46460  pwsal  46555  salexct  46574  sge0fodjrnlem  46656  iundjiun  46700  meaunle  46704  meadjiunlem  46705  meaiunlelem  46708  meadif  46719  meaiuninclem  46720  meaiininclem  46726  carageniuncllem2  46762  caragencmpl  46775  hsphoidmvle2  46825  hsphoidmvle  46826  hoidmv1lelem2  46832  hspmbllem1  46866  hspmbllem3  46868  uhgrimisgrgric  48173  fdmdifeqresdif  48584  lincdifsn  48666  lincresunit2  48720  lincresunit3lem2  48722  iscnrm3rlem3  49183  iscnrm3rlem7  49187