Theorem difssd 4091

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3902   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-ss 3922

This theorem is referenced by:  uneqdifeq  4453  fpr1  8296  fofinf1o  9285  ackbij1lem12  10209  ssfin4  10289  enfin1ai  10363  fpwwe2  10623  wundif  10694  cshimadifsn  14862  indsum  15876  fprodn0f  16041  rpnnen2lem11  16275  mrieqvlemd  17680  mrieqv2d  17690  symgextfo  19487  symgextres  19490  symgfixelsi  19500  pmtrdifellem1  19541  pmtrdifellem2  19542  dprdfeq0  20089  dpjf  20124  dpjlid  20128  dpjghm  20130  ablfac1eu  20140  isdrng3lem1  20851  subdrgint  20906  islbs3  21279  lbsextlem4  21285  cnflddiv  21552  frlmsslss2  21925  frlmlbs  21947  selvvvval  22293  psdmul  22329  mdetrlin  22759  mdetrsca  22760  mdetralt  22765  mdetmul  22780  smadiadetlem3lem0  22822  smadiadet  22827  clsval2  23207  hausllycmp  23651  qtoprest  23874  trfil3  24045  ufileu  24076  fclscf  24182  alexsublem  24201  blcld  24662  restmetu  24727  evth  25118  lebnumlem1  25120  lebnumlem2  25121  lebnumlem3  25122  cmmbl  25693  nulmbl2  25695  volinun  25705  volsup  25715  uniioombllem3  25744  uniioombllem5  25746  uniioombl  25748  itg1addlem5  25859  itg2cnlem2  25921  dvreslem  26068  dvres2lem  26069  dvaddbr  26097  dvmulbr  26098  dvrec  26114  dvexp3  26137  dveflem  26138  dvcnvrelem2  26177  uhgrspan1  29653  unidifsnel  32881  fdifsupp  33030  fdifsuppconst  33034  fmptunsnop  33045  fprodeq02  33168  indsumin  33181  gsumhashmul  33387  suppgsumssiun  33392  symgcom2  33404  cycpmconjvlem  33461  domnprodn0  33598  dflringlem2  33785  rprmdvdsprod  33824  zringfrac  33844  ply1coedeg  33879  selvascl  33907  selvply1rhm0  33916  extvfvvcl  33925  extvfvcl  33926  evlextv  33932  psrmonprod  33942  esplyind  33965  esplyindfv  33966  esplyfvn  33967  vieta  33970  lindsunlem  34014  dimkerim  34017  madjusmdetlem1  34217  ist0cld  34223  esumpad  34445  esumpad2  34446  measiun  34608  difelcarsg  34700  carsgclctunlem2  34709  tgoldbachgtde  35047  f1resrcmplf1d  35475  satfv1lem  35854  dmopab3rexdif  35897  mthmpps  36074  dvreasin  38377  dvreacos  38378  areacirclem4  38382  sticksstones22  42955  evlselvlem  43340  evlselv  43341  ntrclsrcomplex  44781  ntrclsfveq1  44806  ntrclsiso  44813  ntrclsk2  44814  ntrclskb  44815  ntrclsk3  44816  ntrclsk13  44817  ntrneircomplex  44820  clsneircomplex  44849  clsneiel1  44854  neicvgrcomplex  44859  neicvgel1  44865  difmap  45943  difmapsn  45948  supminfxr2  46203  iccdifprioo  46252  limciccioolb  46357  lptioo2  46367  lptioo1  46368  limcicciooub  46371  dvdivcncf  46661  itgvol0  46702  itgcoscmulx  46703  itgsincmulx  46708  ismbl3  46720  stoweidlem28  46762  stoweidlem50  46784  dirkeritg  46836  dirkercncflem2  46838  dirkercncflem4  46840  fourierdlem39  46880  fourierdlem58  46898  fourierdlem68  46908  fourierdlem76  46916  fourierdlem102  46942  fourierdlem114  46954  pwsal  47049  salexct  47068  sge0fodjrnlem  47150  iundjiun  47194  meaunle  47198  meadjiunlem  47199  meaiunlelem  47202  meadif  47213  meaiuninclem  47214  meaiininclem  47220  carageniuncllem2  47256  caragencmpl  47269  hsphoidmvle2  47319  hsphoidmvle  47320  hoidmv1lelem2  47326  hspmbllem1  47360  hspmbllem3  47362  uhgrimisgrgric  48716  fdmdifeqresdif  49142  lincdifsn  49224  lincresunit2  49278  lincresunit3lem2  49280  iscnrm3rlem3  49740  iscnrm3rlem7  49744