Theorem difssd 4087

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3896   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902  df-ss 3916

This theorem is referenced by:  uneqdifeq  4443  fpr1  8243  fofinf1o  9230  ackbij1lem12  10138  ssfin4  10218  enfin1ai  10292  fpwwe2  10552  wundif  10623  cshimadifsn  14750  fprodn0f  15912  rpnnen2lem11  16147  mrieqvlemd  17550  mrieqv2d  17560  symgextfo  19349  symgextres  19352  symgfixelsi  19362  pmtrdifellem1  19403  pmtrdifellem2  19404  dprdfeq0  19951  dpjf  19986  dpjlid  19990  dpjghm  19992  ablfac1eu  20002  subdrgint  20734  islbs3  21108  lbsextlem4  21114  cnflddiv  21353  frlmsslss2  21728  frlmlbs  21750  psdmul  22107  mdetrlin  22544  mdetrsca  22545  mdetralt  22550  mdetmul  22565  smadiadetlem3lem0  22607  smadiadet  22612  clsval2  22992  hausllycmp  23436  qtoprest  23659  trfil3  23830  ufileu  23861  fclscf  23967  alexsublem  23986  blcld  24447  restmetu  24512  evth  24912  lebnumlem1  24914  lebnumlem2  24915  lebnumlem3  24916  cmmbl  25489  nulmbl2  25491  volinun  25501  volsup  25511  uniioombllem3  25540  uniioombllem5  25542  uniioombl  25544  itg1addlem5  25655  itg2cnlem2  25717  dvreslem  25864  dvres2lem  25865  dvaddbr  25894  dvmulbr  25895  dvmulbrOLD  25896  dvrec  25913  dvexp3  25936  dveflem  25937  dvcnvrelem2  25977  uhgrspan1  29325  unidifsnel  32559  fdifsupp  32713  fdifsuppconst  32717  fmptunsnop  32728  fprodeq02  32853  indsum  32891  indsumin  32892  gsumhashmul  33099  symgcom2  33115  cycpmconjvlem  33172  domnprodn0  33306  rprmdvdsprod  33564  zringfrac  33584  ply1coedeg  33619  extvfvvcl  33649  extvfvcl  33650  evlextv  33656  esplyind  33680  esplyindfv  33681  esplyfvn  33682  vieta  33685  lindsunlem  33730  dimkerim  33733  madjusmdetlem1  33933  ist0cld  33939  esumpad  34161  esumpad2  34162  measiun  34324  difelcarsg  34416  carsgclctunlem2  34425  tgoldbachgtde  34766  f1resrcmplf1d  35192  satfv1lem  35505  dmopab3rexdif  35548  mthmpps  35725  dvreasin  37846  dvreacos  37847  areacirclem4  37851  sticksstones22  42361  selvvvval  42770  evlselvlem  42771  evlselv  42772  ntrclsrcomplex  44218  ntrclsfveq1  44243  ntrclsiso  44250  ntrclsk2  44251  ntrclskb  44252  ntrclsk3  44253  ntrclsk13  44254  ntrneircomplex  44257  clsneircomplex  44286  clsneiel1  44291  neicvgrcomplex  44296  neicvgel1  44302  difmap  45393  difmapsn  45398  supminfxr2  45655  iccdifprioo  45704  limciccioolb  45809  lptioo2  45819  lptioo1  45820  limcicciooub  45823  dvdivcncf  46113  itgvol0  46154  itgcoscmulx  46155  itgsincmulx  46160  ismbl3  46172  stoweidlem28  46214  stoweidlem50  46236  dirkeritg  46288  dirkercncflem2  46290  dirkercncflem4  46292  fourierdlem39  46332  fourierdlem58  46350  fourierdlem68  46360  fourierdlem76  46368  fourierdlem102  46394  fourierdlem114  46406  pwsal  46501  salexct  46520  sge0fodjrnlem  46602  iundjiun  46646  meaunle  46650  meadjiunlem  46651  meaiunlelem  46654  meadif  46665  meaiuninclem  46666  meaiininclem  46672  carageniuncllem2  46708  caragencmpl  46721  hsphoidmvle2  46771  hsphoidmvle  46772  hoidmv1lelem2  46778  hspmbllem1  46812  hspmbllem3  46814  uhgrimisgrgric  48119  fdmdifeqresdif  48530  lincdifsn  48612  lincresunit2  48666  lincresunit3lem2  48668  iscnrm3rlem3  49129  iscnrm3rlem7  49133