Theorem difssd 4103

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3914   ⊆ wss 3917

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-ss 3934

This theorem is referenced by:  uneqdifeq  4459  fpr1  8285  fofinf1o  9290  ackbij1lem12  10190  ssfin4  10270  enfin1ai  10344  fpwwe2  10603  wundif  10674  cshimadifsn  14802  fprodn0f  15964  rpnnen2lem11  16199  mrieqvlemd  17597  mrieqv2d  17607  symgextfo  19359  symgextres  19362  symgfixelsi  19372  pmtrdifellem1  19413  pmtrdifellem2  19414  dprdfeq0  19961  dpjf  19996  dpjlid  20000  dpjghm  20002  ablfac1eu  20012  subdrgint  20719  islbs3  21072  lbsextlem4  21078  cnflddiv  21319  frlmsslss2  21691  frlmlbs  21713  psdmul  22060  mdetrlin  22496  mdetrsca  22497  mdetralt  22502  mdetmul  22517  smadiadetlem3lem0  22559  smadiadet  22564  clsval2  22944  hausllycmp  23388  qtoprest  23611  trfil3  23782  ufileu  23813  fclscf  23919  alexsublem  23938  blcld  24400  restmetu  24465  evth  24865  lebnumlem1  24867  lebnumlem2  24868  lebnumlem3  24869  cmmbl  25442  nulmbl2  25444  volinun  25454  volsup  25464  uniioombllem3  25493  uniioombllem5  25495  uniioombl  25497  itg1addlem5  25608  itg2cnlem2  25670  dvreslem  25817  dvres2lem  25818  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvrec  25866  dvexp3  25889  dveflem  25890  dvcnvrelem2  25930  uhgrspan1  29237  unidifsnel  32471  fdifsupp  32615  fdifsuppconst  32619  fmptunsnop  32630  fprodeq02  32755  indsum  32791  indsumin  32792  gsumhashmul  33008  symgcom2  33048  cycpmconjvlem  33105  domnprodn0  33233  rprmdvdsprod  33512  zringfrac  33532  lindsunlem  33627  dimkerim  33630  madjusmdetlem1  33824  ist0cld  33830  esumpad  34052  esumpad2  34053  measiun  34215  difelcarsg  34308  carsgclctunlem2  34317  tgoldbachgtde  34658  f1resrcmplf1d  35084  satfv1lem  35356  dmopab3rexdif  35399  mthmpps  35576  dvreasin  37707  dvreacos  37708  areacirclem4  37712  sticksstones22  42163  selvvvval  42580  evlselvlem  42581  evlselv  42582  ntrclsrcomplex  44031  ntrclsfveq1  44056  ntrclsiso  44063  ntrclsk2  44064  ntrclskb  44065  ntrclsk3  44066  ntrclsk13  44067  ntrneircomplex  44070  clsneircomplex  44099  clsneiel1  44104  neicvgrcomplex  44109  neicvgel1  44115  difmap  45208  difmapsn  45213  supminfxr2  45472  iccdifprioo  45521  limciccioolb  45626  lptioo2  45636  lptioo1  45637  limcicciooub  45642  dvdivcncf  45932  itgvol0  45973  itgcoscmulx  45974  itgsincmulx  45979  ismbl3  45991  stoweidlem28  46033  stoweidlem50  46055  dirkeritg  46107  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem39  46151  fourierdlem58  46169  fourierdlem68  46179  fourierdlem76  46187  fourierdlem102  46213  fourierdlem114  46225  pwsal  46320  salexct  46339  sge0fodjrnlem  46421  iundjiun  46465  meaunle  46469  meadjiunlem  46470  meaiunlelem  46473  meadif  46484  meaiuninclem  46485  meaiininclem  46491  carageniuncllem2  46527  caragencmpl  46540  hsphoidmvle2  46590  hsphoidmvle  46591  hoidmv1lelem2  46597  hspmbllem1  46631  hspmbllem3  46633  uhgrimisgrgric  47935  fdmdifeqresdif  48334  lincdifsn  48417  lincresunit2  48471  lincresunit3lem2  48473  iscnrm3rlem3  48934  iscnrm3rlem7  48938