Theorem difssd 4078

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3887   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-ss 3907

This theorem is referenced by:  uneqdifeq  4433  fpr1  8247  fofinf1o  9236  ackbij1lem12  10146  ssfin4  10226  enfin1ai  10300  fpwwe2  10560  wundif  10631  cshimadifsn  14785  indsum  15785  fprodn0f  15950  rpnnen2lem11  16185  mrieqvlemd  17589  mrieqv2d  17599  symgextfo  19391  symgextres  19394  symgfixelsi  19404  pmtrdifellem1  19445  pmtrdifellem2  19446  dprdfeq0  19993  dpjf  20028  dpjlid  20032  dpjghm  20034  ablfac1eu  20044  subdrgint  20774  islbs3  21148  lbsextlem4  21154  cnflddiv  21393  frlmsslss2  21768  frlmlbs  21790  psdmul  22145  mdetrlin  22580  mdetrsca  22581  mdetralt  22586  mdetmul  22601  smadiadetlem3lem0  22643  smadiadet  22648  clsval2  23028  hausllycmp  23472  qtoprest  23695  trfil3  23866  ufileu  23897  fclscf  24003  alexsublem  24022  blcld  24483  restmetu  24548  evth  24939  lebnumlem1  24941  lebnumlem2  24942  lebnumlem3  24943  cmmbl  25514  nulmbl2  25516  volinun  25526  volsup  25536  uniioombllem3  25565  uniioombllem5  25567  uniioombl  25569  itg1addlem5  25680  itg2cnlem2  25742  dvreslem  25889  dvres2lem  25890  dvaddbr  25918  dvmulbr  25919  dvrec  25935  dvexp3  25958  dveflem  25959  dvcnvrelem2  25998  uhgrspan1  29389  unidifsnel  32623  fdifsupp  32776  fdifsuppconst  32780  fmptunsnop  32791  fprodeq02  32915  indsumin  32939  gsumhashmul  33146  suppgsumssiun  33151  symgcom2  33163  cycpmconjvlem  33220  domnprodn0  33354  rprmdvdsprod  33612  zringfrac  33632  ply1coedeg  33667  extvfvvcl  33697  extvfvcl  33698  evlextv  33704  psrmonprod  33714  esplyind  33737  esplyindfv  33738  esplyfvn  33739  vieta  33742  lindsunlem  33787  dimkerim  33790  madjusmdetlem1  33990  ist0cld  33996  esumpad  34218  esumpad2  34219  measiun  34381  difelcarsg  34473  carsgclctunlem2  34482  tgoldbachgtde  34823  f1resrcmplf1d  35249  satfv1lem  35563  dmopab3rexdif  35606  mthmpps  35783  dvreasin  38044  dvreacos  38045  areacirclem4  38049  sticksstones22  42624  selvvvval  43035  evlselvlem  43036  evlselv  43037  ntrclsrcomplex  44483  ntrclsfveq1  44508  ntrclsiso  44515  ntrclsk2  44516  ntrclskb  44517  ntrclsk3  44518  ntrclsk13  44519  ntrneircomplex  44522  clsneircomplex  44551  clsneiel1  44556  neicvgrcomplex  44561  neicvgel1  44567  difmap  45657  difmapsn  45662  supminfxr2  45918  iccdifprioo  45967  limciccioolb  46072  lptioo2  46082  lptioo1  46083  limcicciooub  46086  dvdivcncf  46376  itgvol0  46417  itgcoscmulx  46418  itgsincmulx  46423  ismbl3  46435  stoweidlem28  46477  stoweidlem50  46499  dirkeritg  46551  dirkercncflem2  46553  dirkercncflem4  46555  fourierdlem39  46595  fourierdlem58  46613  fourierdlem68  46623  fourierdlem76  46631  fourierdlem102  46657  fourierdlem114  46669  pwsal  46764  salexct  46783  sge0fodjrnlem  46865  iundjiun  46909  meaunle  46913  meadjiunlem  46914  meaiunlelem  46917  meadif  46928  meaiuninclem  46929  meaiininclem  46935  carageniuncllem2  46971  caragencmpl  46984  hsphoidmvle2  47034  hsphoidmvle  47035  hoidmv1lelem2  47041  hspmbllem1  47075  hspmbllem3  47077  uhgrimisgrgric  48422  fdmdifeqresdif  48833  lincdifsn  48915  lincresunit2  48969  lincresunit3lem2  48971  iscnrm3rlem3  49432  iscnrm3rlem7  49436