Theorem difssd 4112

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3923   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-ss 3943

This theorem is referenced by:  uneqdifeq  4468  fpr1  8300  fofinf1o  9342  ackbij1lem12  10242  ssfin4  10322  enfin1ai  10396  fpwwe2  10655  wundif  10726  cshimadifsn  14846  fprodn0f  16005  rpnnen2lem11  16240  mrieqvlemd  17639  mrieqv2d  17649  symgextfo  19401  symgextres  19404  symgfixelsi  19414  pmtrdifellem1  19455  pmtrdifellem2  19456  dprdfeq0  20003  dpjf  20038  dpjlid  20042  dpjghm  20044  ablfac1eu  20054  subdrgint  20761  islbs3  21114  lbsextlem4  21120  cnflddiv  21361  frlmsslss2  21733  frlmlbs  21755  psdmul  22102  mdetrlin  22538  mdetrsca  22539  mdetralt  22544  mdetmul  22559  smadiadetlem3lem0  22601  smadiadet  22606  clsval2  22986  hausllycmp  23430  qtoprest  23653  trfil3  23824  ufileu  23855  fclscf  23961  alexsublem  23980  blcld  24442  restmetu  24507  evth  24907  lebnumlem1  24909  lebnumlem2  24910  lebnumlem3  24911  cmmbl  25485  nulmbl2  25487  volinun  25497  volsup  25507  uniioombllem3  25536  uniioombllem5  25538  uniioombl  25540  itg1addlem5  25651  itg2cnlem2  25713  dvreslem  25860  dvres2lem  25861  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvrec  25909  dvexp3  25932  dveflem  25933  dvcnvrelem2  25973  uhgrspan1  29228  unidifsnel  32462  fdifsupp  32608  fdifsuppconst  32612  fmptunsnop  32623  fprodeq02  32748  indsum  32784  indsumin  32785  gsumhashmul  33001  symgcom2  33041  cycpmconjvlem  33098  domnprodn0  33216  rprmdvdsprod  33495  zringfrac  33515  lindsunlem  33610  dimkerim  33613  madjusmdetlem1  33804  ist0cld  33810  esumpad  34032  esumpad2  34033  measiun  34195  difelcarsg  34288  carsgclctunlem2  34297  tgoldbachgtde  34638  f1resrcmplf1d  35064  satfv1lem  35330  dmopab3rexdif  35373  mthmpps  35550  dvreasin  37676  dvreacos  37677  areacirclem4  37681  sticksstones22  42127  selvvvval  42555  evlselvlem  42556  evlselv  42557  ntrclsrcomplex  44006  ntrclsfveq1  44031  ntrclsiso  44038  ntrclsk2  44039  ntrclskb  44040  ntrclsk3  44041  ntrclsk13  44042  ntrneircomplex  44045  clsneircomplex  44074  clsneiel1  44079  neicvgrcomplex  44084  neicvgel1  44090  difmap  45179  difmapsn  45184  supminfxr2  45444  iccdifprioo  45493  limciccioolb  45598  lptioo2  45608  lptioo1  45609  limcicciooub  45614  dvdivcncf  45904  itgvol0  45945  itgcoscmulx  45946  itgsincmulx  45951  ismbl3  45963  stoweidlem28  46005  stoweidlem50  46027  dirkeritg  46079  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem39  46123  fourierdlem58  46141  fourierdlem68  46151  fourierdlem76  46159  fourierdlem102  46185  fourierdlem114  46197  pwsal  46292  salexct  46311  sge0fodjrnlem  46393  iundjiun  46437  meaunle  46441  meadjiunlem  46442  meaiunlelem  46445  meadif  46456  meaiuninclem  46457  meaiininclem  46463  carageniuncllem2  46499  caragencmpl  46512  hsphoidmvle2  46562  hsphoidmvle  46563  hoidmv1lelem2  46569  hspmbllem1  46603  hspmbllem3  46605  uhgrimisgrgric  47892  fdmdifeqresdif  48265  lincdifsn  48348  lincresunit2  48402  lincresunit3lem2  48404  iscnrm3rlem3  48864  iscnrm3rlem7  48868