Theorem difssd 4076

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

Assertion

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

Proof of Theorem difssd

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900   ∖ cdif 4048

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-dif 4050

This theorem is used by:  uneqdifeq  4451  f1resrcmplf1d  7310  fpr1  8359  fofinf1o  9359  ackbij1lem12  10347  ssfin4  10427  enfin1ai  10501  fpwwe2  10767  wundif  10838  cshimadifsn  15022  indsum  16039  fprodn0f  16202  rpnnen2lem11  16436  mrieqvlemd  17853  mrieqv2d  17863  symgextfo  19687  symgextres  19690  symgfixelsi  19700  pmtrdifellem1  19741  pmtrdifellem2  19742  dprdfeq0  20289  dpjf  20324  dpjlid  20328  dpjghm  20330  ablfac1eu  20340  isdrng3lem1  21056  subdrgint  21111  islbs3  21484  lbsextlem4  21490  cnflddiv  21760  frlmsslss2  22136  frlmlbs  22158  selvvvval  22506  psdmul  22542  mdetrlin  22972  mdetrsca  22973  mdetralt  22978  mdetmul  22993  smadiadetlem3lem0  23035  smadiadet  23040  clsval2  23423  hausllycmp  23868  qtoprest  24091  trfil3  24262  ufileu  24293  fclscf  24399  alexsublem  24418  blcld  24879  restmetu  24944  evth  25335  lebnumlem1  25337  lebnumlem2  25338  lebnumlem3  25339  cmmbl  25910  nulmbl2  25912  volinun  25922  volsup  25932  uniioombllem3  25961  uniioombllem5  25963  uniioombl  25965  itg1addlem5  26076  itg2cnlem2  26138  dvreslem  26284  dvres2lem  26285  dvaddbr  26313  dvmulbr  26314  dvrec  26330  dvexp3  26353  dveflem  26354  dvcnvrelem2  26393  uhgrspan1  29941  unidifsnel  33229  fdifsupp  33375  fdifsuppconst  33379  fmptunsnop  33390  fprodeq02  33511  indsumin  33524  gsumhashmul  33727  suppgsumssiun  33732  symgcom2  33744  cycpmconjvlem  33801  domnprodn0  33938  fldedom  33956  zzedom  33958  ply1edom  33959  dflringlem2  34131  rprmdvdsprod  34170  zringfrac  34189  ply1coedeg  34224  selvascl  34260  selvply1rhm0  34269  extvfvvcl  34278  extvfvcl  34279  evlextv  34285  psrmonprod  34295  esplyind  34318  esplyindfv  34319  esplyfvn  34320  vieta  34323  lindsunlem  34367  dimkerim  34370  madjusmdetlem1  34570  ist0cld  34576  esumpad  34798  esumpad2  34799  measiun  34962  difelcarsg  35053  carsgclctunlem2  35062  tgoldbachgtde  35400  satfv1lem  36335  dmopab3rexdif  36378  mthmpps  36555  dvreasin  38892  dvreacos  38893  areacirclem4  38897  sticksstones22  43484  evlselvlem  43882  evlselv  43883  ntrclsrcomplex  45296  ntrclsfveq1  45321  ntrclsiso  45328  ntrclsk2  45329  ntrclskb  45330  ntrclsk3  45331  ntrclsk13  45332  ntrneircomplex  45335  clsneircomplex  45364  clsneiel1  45369  neicvgrcomplex  45374  neicvgel1  45380  difmap  46493  difmapsn  46498  supminfxr2  46752  iccdifprioo  46801  limciccioolb  46906  lptioo2  46916  lptioo1  46917  limcicciooub  46920  dvdivcncf  47210  itgvol0  47251  itgcoscmulx  47252  itgsincmulx  47257  ismbl3  47269  stoweidlem28  47311  stoweidlem50  47333  dirkeritg  47385  dirkercncflem2  47387  dirkercncflem4  47389  fourierdlem39  47429  fourierdlem58  47447  fourierdlem68  47457  fourierdlem76  47465  fourierdlem102  47491  fourierdlem114  47503  pwsal  47598  salexct  47617  sge0fodjrnlem  47699  iundjiun  47743  meaunle  47747  meadjiunlem  47748  meaiunlelem  47751  meadif  47762  meaiuninclem  47763  meaiininclem  47769  carageniuncllem2  47805  caragencmpl  47818  hsphoidmvle2  47868  hsphoidmvle  47869  hoidmv1lelem2  47875  hspmbllem1  47909  hspmbllem3  47911  uhgrimisgrgric  49302  fdmdifeqresdif  49785  lincdifsn  49867  lincresunit2  49921  lincresunit3lem2  49923  iscnrm3rlem3  50387  iscnrm3rlem7  50391