Theorem difssd 4040

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3857   ⊆ wss 3860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-dif 3863  df-in 3867  df-ss 3877

This theorem is referenced by:  uneqdifeq  4389  fofinf1o  8845  ackbij1lem12  9704  ssfin4  9783  enfin1ai  9857  fpwwe2  10116  wundif  10187  cshimadifsn  14251  fprodn0f  15406  rpnnen2lem11  15638  mrieqvlemd  16972  mrieqv2d  16982  symgextfo  18631  symgextres  18634  symgfixelsi  18644  pmtrdifellem1  18685  pmtrdifellem2  18686  dprdfeq0  19226  dpjf  19261  dpjlid  19265  dpjghm  19267  ablfac1eu  19277  subdrgint  19664  islbs3  20009  lbsextlem4  20015  frlmsslss2  20554  frlmlbs  20576  mdetrlin  21316  mdetrsca  21317  mdetralt  21322  mdetmul  21337  smadiadetlem3lem0  21379  smadiadet  21384  clsval2  21764  hausllycmp  22208  qtoprest  22431  trfil3  22602  ufileu  22633  fclscf  22739  alexsublem  22758  blcld  23221  restmetu  23286  evth  23674  lebnumlem1  23676  lebnumlem2  23677  lebnumlem3  23678  cmmbl  24248  nulmbl2  24250  volinun  24260  volsup  24270  uniioombllem3  24299  uniioombllem5  24301  uniioombl  24303  itg1addlem5  24414  itg2cnlem2  24476  dvreslem  24622  dvres2lem  24623  dvaddbr  24651  dvmulbr  24652  dvrec  24668  dvexp3  24691  dveflem  24692  dvcnvrelem2  24731  uhgrspan1  27206  unidifsnel  30419  fdifsuppconst  30560  fprodeq02  30674  gsumhashmul  30855  symgcom2  30892  cycpmconjvlem  30947  lindsunlem  31239  dimkerim  31242  madjusmdetlem1  31311  ist0cld  31317  indsum  31521  indsumin  31522  esumpad  31555  esumpad2  31556  measiun  31718  difelcarsg  31809  carsgclctunlem2  31818  tgoldbachgtde  32172  f1resrcmplf1d  32592  satfv1lem  32853  dmopab3rexdif  32896  mthmpps  33073  fpr1  33414  dvreasin  35458  dvreacos  35459  areacirclem4  35463  ntrclsrcomplex  41156  ntrclsfveq1  41181  ntrclsiso  41188  ntrclsk2  41189  ntrclskb  41190  ntrclsk3  41191  ntrclsk13  41192  ntrneircomplex  41195  clsneircomplex  41224  clsneiel1  41229  neicvgrcomplex  41234  neicvgel1  41240  difmap  42251  difmapsn  42256  supminfxr2  42519  iccdifprioo  42564  limciccioolb  42674  lptioo2  42684  lptioo1  42685  limcicciooub  42690  dvdivcncf  42980  itgvol0  43021  itgcoscmulx  43022  itgsincmulx  43027  ismbl3  43039  stoweidlem28  43081  stoweidlem50  43103  dirkeritg  43155  dirkercncflem2  43157  dirkercncflem4  43159  fourierdlem39  43199  fourierdlem58  43217  fourierdlem68  43227  fourierdlem76  43235  fourierdlem102  43261  fourierdlem114  43273  pwsal  43368  salexct  43385  sge0fodjrnlem  43466  iundjiun  43510  meaunle  43514  meadjiunlem  43515  meaiunlelem  43518  meadif  43529  meaiuninclem  43530  meaiininclem  43536  carageniuncllem2  43572  caragencmpl  43585  hsphoidmvle2  43635  hsphoidmvle  43636  hoidmv1lelem2  43642  hspmbllem1  43676  hspmbllem3  43678  fdmdifeqresdif  45169  lincdifsn  45257  lincresunit2  45311  lincresunit3lem2  45313  iscnrm3rlem3  45687  iscnrm3rlem7  45691