Theorem difssd 4072

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

Assertion

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

Proof of Theorem difssd

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-dif 4046

This theorem is used by:  uneqdifeq  4447  f1resrcmplf1d  7283  fpr1  8329  fofinf1o  9329  ackbij1lem12  10315  ssfin4  10395  enfin1ai  10469  fpwwe2  10735  wundif  10806  cshimadifsn  14988  indsum  16004  fprodn0f  16167  rpnnen2lem11  16401  mrieqvlemd  17812  mrieqv2d  17822  symgextfo  19645  symgextres  19648  symgfixelsi  19658  pmtrdifellem1  19699  pmtrdifellem2  19700  dprdfeq0  20247  dpjf  20282  dpjlid  20286  dpjghm  20288  ablfac1eu  20298  isdrng3lem1  21014  subdrgint  21069  islbs3  21442  lbsextlem4  21448  cnflddiv  21717  frlmsslss2  22090  frlmlbs  22112  selvvvval  22460  psdmul  22496  mdetrlin  22926  mdetrsca  22927  mdetralt  22932  mdetmul  22947  smadiadetlem3lem0  22989  smadiadet  22994  clsval2  23377  hausllycmp  23822  qtoprest  24045  trfil3  24216  ufileu  24247  fclscf  24353  alexsublem  24372  blcld  24833  restmetu  24898  evth  25289  lebnumlem1  25291  lebnumlem2  25292  lebnumlem3  25293  cmmbl  25864  nulmbl2  25866  volinun  25876  volsup  25886  uniioombllem3  25915  uniioombllem5  25917  uniioombl  25919  itg1addlem5  26030  itg2cnlem2  26092  dvreslem  26238  dvres2lem  26239  dvaddbr  26267  dvmulbr  26268  dvrec  26284  dvexp3  26307  dveflem  26308  dvcnvrelem2  26347  uhgrspan1  29893  unidifsnel  33182  fdifsupp  33329  fdifsuppconst  33333  fmptunsnop  33344  fprodeq02  33465  indsumin  33478  gsumhashmul  33678  suppgsumssiun  33683  symgcom2  33695  cycpmconjvlem  33752  domnprodn0  33889  dflringlem2  34077  rprmdvdsprod  34116  zringfrac  34136  ply1coedeg  34171  selvascl  34199  selvply1rhm0  34208  extvfvvcl  34217  extvfvcl  34218  evlextv  34224  psrmonprod  34234  esplyind  34257  esplyindfv  34258  esplyfvn  34259  vieta  34262  lindsunlem  34306  dimkerim  34309  madjusmdetlem1  34509  ist0cld  34515  esumpad  34737  esumpad2  34738  measiun  34901  difelcarsg  34992  carsgclctunlem2  35001  tgoldbachgtde  35339  satfv1lem  36245  dmopab3rexdif  36288  mthmpps  36465  dvreasin  38761  dvreacos  38762  areacirclem4  38766  sticksstones22  43355  evlselvlem  43753  evlselv  43754  ntrclsrcomplex  45172  ntrclsfveq1  45197  ntrclsiso  45204  ntrclsk2  45205  ntrclskb  45206  ntrclsk3  45207  ntrclsk13  45208  ntrneircomplex  45211  clsneircomplex  45240  clsneiel1  45245  neicvgrcomplex  45250  neicvgel1  45256  difmap  46356  difmapsn  46361  supminfxr2  46615  iccdifprioo  46664  limciccioolb  46769  lptioo2  46779  lptioo1  46780  limcicciooub  46783  dvdivcncf  47073  itgvol0  47114  itgcoscmulx  47115  itgsincmulx  47120  ismbl3  47132  stoweidlem28  47174  stoweidlem50  47196  dirkeritg  47248  dirkercncflem2  47250  dirkercncflem4  47252  fourierdlem39  47292  fourierdlem58  47310  fourierdlem68  47320  fourierdlem76  47328  fourierdlem102  47354  fourierdlem114  47366  pwsal  47461  salexct  47480  sge0fodjrnlem  47562  iundjiun  47606  meaunle  47610  meadjiunlem  47611  meaiunlelem  47614  meadif  47625  meaiuninclem  47626  meaiininclem  47632  carageniuncllem2  47668  caragencmpl  47681  hsphoidmvle2  47731  hsphoidmvle  47732  hoidmv1lelem2  47738  hspmbllem1  47772  hspmbllem3  47774  uhgrimisgrgric  49165  fdmdifeqresdif  49590  lincdifsn  49672  lincresunit2  49726  lincresunit3lem2  49728  iscnrm3rlem3  50192  iscnrm3rlem7  50196