Theorem difssd 4091

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

Assertion

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

Proof of Theorem difssd

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

This proof depends on syntax axioms:   → wi 4   ∖ cdif 3903   ⊆ wss 3906

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-ss 3923

This theorem is used by:  uneqdifeq  4455  f1resrcmplf1d  7278  fpr1  8306  fofinf1o  9296  ackbij1lem12  10229  ssfin4  10309  enfin1ai  10383  fpwwe2  10645  wundif  10716  cshimadifsn  14892  indsum  15905  fprodn0f  16070  rpnnen2lem11  16304  mrieqvlemd  17709  mrieqv2d  17719  symgextfo  19538  symgextres  19541  symgfixelsi  19551  pmtrdifellem1  19592  pmtrdifellem2  19593  dprdfeq0  20140  dpjf  20175  dpjlid  20179  dpjghm  20181  ablfac1eu  20191  isdrng3lem1  20903  subdrgint  20958  islbs3  21331  lbsextlem4  21337  cnflddiv  21604  frlmsslss2  21977  frlmlbs  21999  selvvvval  22345  psdmul  22381  mdetrlin  22811  mdetrsca  22812  mdetralt  22817  mdetmul  22832  smadiadetlem3lem0  22874  smadiadet  22879  clsval2  23259  hausllycmp  23704  qtoprest  23927  trfil3  24098  ufileu  24129  fclscf  24235  alexsublem  24254  blcld  24715  restmetu  24780  evth  25171  lebnumlem1  25173  lebnumlem2  25174  lebnumlem3  25175  cmmbl  25746  nulmbl2  25748  volinun  25758  volsup  25768  uniioombllem3  25797  uniioombllem5  25799  uniioombl  25801  itg1addlem5  25912  itg2cnlem2  25974  dvreslem  26121  dvres2lem  26122  dvaddbr  26150  dvmulbr  26151  dvrec  26167  dvexp3  26190  dveflem  26191  dvcnvrelem2  26230  uhgrspan1  29713  unidifsnel  32954  fdifsupp  33103  fdifsuppconst  33107  fmptunsnop  33118  fprodeq02  33240  indsumin  33253  gsumhashmul  33453  suppgsumssiun  33458  symgcom2  33470  cycpmconjvlem  33527  domnprodn0  33664  dflringlem2  33851  rprmdvdsprod  33890  zringfrac  33910  ply1coedeg  33945  selvascl  33973  selvply1rhm0  33982  extvfvvcl  33991  extvfvcl  33992  evlextv  33998  psrmonprod  34008  esplyind  34031  esplyindfv  34032  esplyfvn  34033  vieta  34036  lindsunlem  34080  dimkerim  34083  madjusmdetlem1  34283  ist0cld  34289  esumpad  34511  esumpad2  34512  measiun  34675  difelcarsg  34767  carsgclctunlem2  34776  tgoldbachgtde  35114  satfv1lem  35893  dmopab3rexdif  35936  mthmpps  36113  dvreasin  38416  dvreacos  38417  areacirclem4  38421  sticksstones22  42995  evlselvlem  43380  evlselv  43381  ntrclsrcomplex  44821  ntrclsfveq1  44846  ntrclsiso  44853  ntrclsk2  44854  ntrclskb  44855  ntrclsk3  44856  ntrclsk13  44857  ntrneircomplex  44860  clsneircomplex  44889  clsneiel1  44894  neicvgrcomplex  44899  neicvgel1  44905  difmap  45983  difmapsn  45988  supminfxr2  46243  iccdifprioo  46292  limciccioolb  46397  lptioo2  46407  lptioo1  46408  limcicciooub  46411  dvdivcncf  46701  itgvol0  46742  itgcoscmulx  46743  itgsincmulx  46748  ismbl3  46760  stoweidlem28  46802  stoweidlem50  46824  dirkeritg  46876  dirkercncflem2  46878  dirkercncflem4  46880  fourierdlem39  46920  fourierdlem58  46938  fourierdlem68  46948  fourierdlem76  46956  fourierdlem102  46982  fourierdlem114  46994  pwsal  47089  salexct  47108  sge0fodjrnlem  47190  iundjiun  47234  meaunle  47238  meadjiunlem  47239  meaiunlelem  47242  meadif  47253  meaiuninclem  47254  meaiininclem  47260  carageniuncllem2  47296  caragencmpl  47309  hsphoidmvle2  47359  hsphoidmvle  47360  hoidmv1lelem2  47366  hspmbllem1  47400  hspmbllem3  47402  uhgrimisgrgric  48756  fdmdifeqresdif  49181  lincdifsn  49263  lincresunit2  49317  lincresunit3lem2  49319  iscnrm3rlem3  49779  iscnrm3rlem7  49783