Theorem difssd 3700

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3537   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554

This theorem is referenced by:  uneqdifeq  4009  fofinf1o  8126  ackbij1lem12  8936  ssfin4  9015  enfin1ai  9089  fpwwe2  9344  wundif  9415  cshimadifsn  13426  fprodn0f  14561  rpnnen2lem11  14792  mrieqvlemd  16112  mrieqv2d  16122  symgextfo  17665  symgextres  17668  symgfixelsi  17678  pmtrdifellem1  17719  pmtrdifellem2  17720  dprdfeq0  18244  dpjf  18279  dpjlid  18283  dpjghm  18285  ablfac1eu  18295  islbs3  18976  lbsextlem4  18982  frlmsslss2  19933  frlmlbs  19955  mdetrlin  20227  mdetrsca  20228  mdetralt  20233  mdetmul  20248  smadiadetlem3lem0  20290  smadiadet  20295  clsval2  20664  hausllycmp  21107  qtoprest  21330  trfil3  21502  ufileu  21533  fclscf  21639  alexsublem  21658  blcld  22120  restmetu  22185  evth  22566  lebnumlem1  22568  lebnumlem2  22569  lebnumlem3  22570  cmmbl  23109  nulmbl2  23111  volinun  23121  volsup  23131  uniioombllem3  23159  uniioombllem5  23161  uniioombl  23163  itg1addlem5  23273  itg2cnlem2  23335  dvreslem  23479  dvres2lem  23480  dvaddbr  23507  dvmulbr  23508  dvrec  23524  dvexp3  23545  dveflem  23546  dvcnvrelem2  23585  madjusmdetlem1  29221  indsum  29412  esumpad  29444  esumpad2  29445  measiun  29608  difelcarsg  29699  carsgclctunlem2  29708  mthmpps  30733  dvreasin  32668  dvreacos  32669  areacirclem4  32673  ntrclsrcomplex  37353  clsk3nimkb  37358  ntrclsfveq1  37378  ntrclsiso  37385  ntrclsk2  37386  ntrclskb  37387  ntrclsk3  37388  ntrclsk13  37389  ntrneircomplex  37392  clsneircomplex  37421  clsneiel1  37426  neicvgrcomplex  37431  neicvgel1  37437  difmap  38394  difmapsn  38399  iccdifprioo  38589  limciccioolb  38688  lptioo2  38698  lptioo1  38699  limcicciooub  38704  dvdivcncf  38817  itgvol0  38860  itgcoscmulx  38861  itgsincmulx  38866  ismbl3  38879  stoweidlem28  38921  stoweidlem50  38943  dirkeritg  38995  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem39  39039  fourierdlem58  39057  fourierdlem68  39067  fourierdlem76  39075  fourierdlem102  39101  fourierdlem114  39113  pwsal  39211  salexct  39228  sge0fodjrnlem  39309  iundjiun  39353  meaunle  39357  meadjiunlem  39358  meaiunlelem  39361  meadif  39372  meaiuninclem  39373  meaiininclem  39376  carageniuncllem2  39412  caragencmpl  39425  hsphoidmvle2  39475  hsphoidmvle  39476  hoidmv1lelem2  39482  hspmbllem1  39516  hspmbllem3  39518  uhgrspan1  40527  fdmdifeqresdif  41913  lincdifsn  42007  lincresunit2  42061  lincresunit3lem2  42063