Theorem difssd 4133

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3946   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966

This theorem is referenced by:  uneqdifeq  4493  fpr1  8288  fofinf1o  9327  ackbij1lem12  10226  ssfin4  10305  enfin1ai  10379  fpwwe2  10638  wundif  10709  cshimadifsn  14780  fprodn0f  15935  rpnnen2lem11  16167  mrieqvlemd  17573  mrieqv2d  17583  symgextfo  19290  symgextres  19293  symgfixelsi  19303  pmtrdifellem1  19344  pmtrdifellem2  19345  dprdfeq0  19892  dpjf  19927  dpjlid  19931  dpjghm  19933  ablfac1eu  19943  subdrgint  20419  islbs3  20768  lbsextlem4  20774  frlmsslss2  21330  frlmlbs  21352  mdetrlin  22104  mdetrsca  22105  mdetralt  22110  mdetmul  22125  smadiadetlem3lem0  22167  smadiadet  22172  clsval2  22554  hausllycmp  22998  qtoprest  23221  trfil3  23392  ufileu  23423  fclscf  23529  alexsublem  23548  blcld  24014  restmetu  24079  evth  24475  lebnumlem1  24477  lebnumlem2  24478  lebnumlem3  24479  cmmbl  25051  nulmbl2  25053  volinun  25063  volsup  25073  uniioombllem3  25102  uniioombllem5  25104  uniioombl  25106  itg1addlem5  25218  itg2cnlem2  25280  dvreslem  25426  dvres2lem  25427  dvaddbr  25455  dvmulbr  25456  dvrec  25472  dvexp3  25495  dveflem  25496  dvcnvrelem2  25535  uhgrspan1  28591  unidifsnel  31803  fdifsuppconst  31942  fprodeq02  32060  gsumhashmul  32239  symgcom2  32276  cycpmconjvlem  32331  lindsunlem  32740  dimkerim  32743  madjusmdetlem1  32838  ist0cld  32844  indsum  33050  indsumin  33051  esumpad  33084  esumpad2  33085  measiun  33247  difelcarsg  33340  carsgclctunlem2  33349  tgoldbachgtde  33703  f1resrcmplf1d  34121  satfv1lem  34384  dmopab3rexdif  34427  mthmpps  34604  gg-dvmulbr  35206  dvreasin  36622  dvreacos  36623  areacirclem4  36627  sticksstones22  41032  selvvvval  41205  evlselvlem  41206  evlselv  41207  ntrclsrcomplex  42834  ntrclsfveq1  42859  ntrclsiso  42866  ntrclsk2  42867  ntrclskb  42868  ntrclsk3  42869  ntrclsk13  42870  ntrneircomplex  42873  clsneircomplex  42902  clsneiel1  42907  neicvgrcomplex  42912  neicvgel1  42918  difmap  43954  difmapsn  43959  supminfxr2  44227  iccdifprioo  44277  limciccioolb  44385  lptioo2  44395  lptioo1  44396  limcicciooub  44401  dvdivcncf  44691  itgvol0  44732  itgcoscmulx  44733  itgsincmulx  44738  ismbl3  44750  stoweidlem28  44792  stoweidlem50  44814  dirkeritg  44866  dirkercncflem2  44868  dirkercncflem4  44870  fourierdlem39  44910  fourierdlem58  44928  fourierdlem68  44938  fourierdlem76  44946  fourierdlem102  44972  fourierdlem114  44984  pwsal  45079  salexct  45098  sge0fodjrnlem  45180  iundjiun  45224  meaunle  45228  meadjiunlem  45229  meaiunlelem  45232  meadif  45243  meaiuninclem  45244  meaiininclem  45250  carageniuncllem2  45286  caragencmpl  45299  hsphoidmvle2  45349  hsphoidmvle  45350  hoidmv1lelem2  45356  hspmbllem1  45390  hspmbllem3  45392  fdmdifeqresdif  47065  lincdifsn  47153  lincresunit2  47207  lincresunit3lem2  47209  iscnrm3rlem3  47623  iscnrm3rlem7  47627