Theorem difssd 4084

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

Assertion

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

Proof of Theorem difssd

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

This proof depends on syntax axioms:   → wi 4   ∖ cdif 3896   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-ss 3916

This theorem is used by:  uneqdifeq  4448  f1resrcmplf1d  7279  fpr1  8321  fofinf1o  9321  ackbij1lem12  10308  ssfin4  10388  enfin1ai  10462  fpwwe2  10728  wundif  10799  cshimadifsn  14980  indsum  15995  fprodn0f  16158  rpnnen2lem11  16392  mrieqvlemd  17803  mrieqv2d  17813  symgextfo  19636  symgextres  19639  symgfixelsi  19649  pmtrdifellem1  19690  pmtrdifellem2  19691  dprdfeq0  20238  dpjf  20273  dpjlid  20277  dpjghm  20279  ablfac1eu  20289  isdrng3lem1  21005  subdrgint  21060  islbs3  21433  lbsextlem4  21439  cnflddiv  21708  frlmsslss2  22081  frlmlbs  22103  selvvvval  22451  psdmul  22487  mdetrlin  22917  mdetrsca  22918  mdetralt  22923  mdetmul  22938  smadiadetlem3lem0  22980  smadiadet  22985  clsval2  23368  hausllycmp  23813  qtoprest  24036  trfil3  24207  ufileu  24238  fclscf  24344  alexsublem  24363  blcld  24824  restmetu  24889  evth  25280  lebnumlem1  25282  lebnumlem2  25283  lebnumlem3  25284  cmmbl  25855  nulmbl2  25857  volinun  25867  volsup  25877  uniioombllem3  25906  uniioombllem5  25908  uniioombl  25910  itg1addlem5  26021  itg2cnlem2  26083  dvreslem  26229  dvres2lem  26230  dvaddbr  26258  dvmulbr  26259  dvrec  26275  dvexp3  26298  dveflem  26299  dvcnvrelem2  26338  uhgrspan1  29884  unidifsnel  33131  fdifsupp  33278  fdifsuppconst  33282  fmptunsnop  33293  fprodeq02  33415  indsumin  33428  gsumhashmul  33628  suppgsumssiun  33633  symgcom2  33645  cycpmconjvlem  33702  domnprodn0  33839  dflringlem2  34027  rprmdvdsprod  34066  zringfrac  34086  ply1coedeg  34121  selvascl  34149  selvply1rhm0  34158  extvfvvcl  34167  extvfvcl  34168  evlextv  34174  psrmonprod  34184  esplyind  34207  esplyindfv  34208  esplyfvn  34209  vieta  34212  lindsunlem  34256  dimkerim  34259  madjusmdetlem1  34459  ist0cld  34465  esumpad  34687  esumpad2  34688  measiun  34851  difelcarsg  34942  carsgclctunlem2  34951  tgoldbachgtde  35289  satfv1lem  36127  dmopab3rexdif  36170  mthmpps  36347  dvreasin  38624  dvreacos  38625  areacirclem4  38629  sticksstones22  43218  evlselvlem  43616  evlselv  43617  ntrclsrcomplex  45034  ntrclsfveq1  45059  ntrclsiso  45066  ntrclsk2  45067  ntrclskb  45068  ntrclsk3  45069  ntrclsk13  45070  ntrneircomplex  45073  clsneircomplex  45102  clsneiel1  45107  neicvgrcomplex  45112  neicvgel1  45118  difmap  46219  difmapsn  46224  supminfxr2  46478  iccdifprioo  46527  limciccioolb  46632  lptioo2  46642  lptioo1  46643  limcicciooub  46646  dvdivcncf  46936  itgvol0  46977  itgcoscmulx  46978  itgsincmulx  46983  ismbl3  46995  stoweidlem28  47037  stoweidlem50  47059  dirkeritg  47111  dirkercncflem2  47113  dirkercncflem4  47115  fourierdlem39  47155  fourierdlem58  47173  fourierdlem68  47183  fourierdlem76  47191  fourierdlem102  47217  fourierdlem114  47229  pwsal  47324  salexct  47343  sge0fodjrnlem  47425  iundjiun  47469  meaunle  47473  meadjiunlem  47474  meaiunlelem  47477  meadif  47488  meaiuninclem  47489  meaiininclem  47495  carageniuncllem2  47531  caragencmpl  47544  hsphoidmvle2  47594  hsphoidmvle  47595  hoidmv1lelem2  47601  hspmbllem1  47635  hspmbllem3  47637  uhgrimisgrgric  49028  fdmdifeqresdif  49453  lincdifsn  49535  lincresunit2  49589  lincresunit3lem2  49591  iscnrm3rlem3  50049  iscnrm3rlem7  50053