Theorem difssd 4096

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3908   ⊆ wss 3911

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-ss 3928

This theorem is referenced by:  uneqdifeq  4452  fpr1  8259  fofinf1o  9259  ackbij1lem12  10159  ssfin4  10239  enfin1ai  10313  fpwwe2  10572  wundif  10643  cshimadifsn  14771  fprodn0f  15933  rpnnen2lem11  16168  mrieqvlemd  17570  mrieqv2d  17580  symgextfo  19336  symgextres  19339  symgfixelsi  19349  pmtrdifellem1  19390  pmtrdifellem2  19391  dprdfeq0  19938  dpjf  19973  dpjlid  19977  dpjghm  19979  ablfac1eu  19989  subdrgint  20723  islbs3  21097  lbsextlem4  21103  cnflddiv  21342  frlmsslss2  21717  frlmlbs  21739  psdmul  22086  mdetrlin  22522  mdetrsca  22523  mdetralt  22528  mdetmul  22543  smadiadetlem3lem0  22585  smadiadet  22590  clsval2  22970  hausllycmp  23414  qtoprest  23637  trfil3  23808  ufileu  23839  fclscf  23945  alexsublem  23964  blcld  24426  restmetu  24491  evth  24891  lebnumlem1  24893  lebnumlem2  24894  lebnumlem3  24895  cmmbl  25468  nulmbl2  25470  volinun  25480  volsup  25490  uniioombllem3  25519  uniioombllem5  25521  uniioombl  25523  itg1addlem5  25634  itg2cnlem2  25696  dvreslem  25843  dvres2lem  25844  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  dvrec  25892  dvexp3  25915  dveflem  25916  dvcnvrelem2  25956  uhgrspan1  29283  unidifsnel  32514  fdifsupp  32658  fdifsuppconst  32662  fmptunsnop  32673  fprodeq02  32798  indsum  32834  indsumin  32835  gsumhashmul  33044  symgcom2  33056  cycpmconjvlem  33113  domnprodn0  33242  rprmdvdsprod  33498  zringfrac  33518  lindsunlem  33613  dimkerim  33616  madjusmdetlem1  33810  ist0cld  33816  esumpad  34038  esumpad2  34039  measiun  34201  difelcarsg  34294  carsgclctunlem2  34303  tgoldbachgtde  34644  f1resrcmplf1d  35070  satfv1lem  35342  dmopab3rexdif  35385  mthmpps  35562  dvreasin  37693  dvreacos  37694  areacirclem4  37698  sticksstones22  42149  selvvvval  42566  evlselvlem  42567  evlselv  42568  ntrclsrcomplex  44017  ntrclsfveq1  44042  ntrclsiso  44049  ntrclsk2  44050  ntrclskb  44051  ntrclsk3  44052  ntrclsk13  44053  ntrneircomplex  44056  clsneircomplex  44085  clsneiel1  44090  neicvgrcomplex  44095  neicvgel1  44101  difmap  45194  difmapsn  45199  supminfxr2  45458  iccdifprioo  45507  limciccioolb  45612  lptioo2  45622  lptioo1  45623  limcicciooub  45628  dvdivcncf  45918  itgvol0  45959  itgcoscmulx  45960  itgsincmulx  45965  ismbl3  45977  stoweidlem28  46019  stoweidlem50  46041  dirkeritg  46093  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem39  46137  fourierdlem58  46155  fourierdlem68  46165  fourierdlem76  46173  fourierdlem102  46199  fourierdlem114  46211  pwsal  46306  salexct  46325  sge0fodjrnlem  46407  iundjiun  46451  meaunle  46455  meadjiunlem  46456  meaiunlelem  46459  meadif  46470  meaiuninclem  46471  meaiininclem  46477  carageniuncllem2  46513  caragencmpl  46526  hsphoidmvle2  46576  hsphoidmvle  46577  hoidmv1lelem2  46583  hspmbllem1  46617  hspmbllem3  46619  uhgrimisgrgric  47924  fdmdifeqresdif  48323  lincdifsn  48406  lincresunit2  48460  lincresunit3lem2  48462  iscnrm3rlem3  48923  iscnrm3rlem7  48927