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 3900   ⊆ wss 3903

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-ss 3920

This theorem is referenced by:  uneqdifeq  4447  fpr1  8255  fofinf1o  9244  ackbij1lem12  10152  ssfin4  10232  enfin1ai  10306  fpwwe2  10566  wundif  10637  cshimadifsn  14764  fprodn0f  15926  rpnnen2lem11  16161  mrieqvlemd  17564  mrieqv2d  17574  symgextfo  19363  symgextres  19366  symgfixelsi  19376  pmtrdifellem1  19417  pmtrdifellem2  19418  dprdfeq0  19965  dpjf  20000  dpjlid  20004  dpjghm  20006  ablfac1eu  20016  subdrgint  20748  islbs3  21122  lbsextlem4  21128  cnflddiv  21367  frlmsslss2  21742  frlmlbs  21764  psdmul  22121  mdetrlin  22558  mdetrsca  22559  mdetralt  22564  mdetmul  22579  smadiadetlem3lem0  22621  smadiadet  22626  clsval2  23006  hausllycmp  23450  qtoprest  23673  trfil3  23844  ufileu  23875  fclscf  23981  alexsublem  24000  blcld  24461  restmetu  24526  evth  24926  lebnumlem1  24928  lebnumlem2  24929  lebnumlem3  24930  cmmbl  25503  nulmbl2  25505  volinun  25515  volsup  25525  uniioombllem3  25554  uniioombllem5  25556  uniioombl  25558  itg1addlem5  25669  itg2cnlem2  25731  dvreslem  25878  dvres2lem  25879  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvrec  25927  dvexp3  25950  dveflem  25951  dvcnvrelem2  25991  uhgrspan1  29388  unidifsnel  32622  fdifsupp  32775  fdifsuppconst  32779  fmptunsnop  32790  fprodeq02  32915  indsum  32953  indsumin  32954  gsumhashmul  33161  suppgsumssiun  33166  symgcom2  33178  cycpmconjvlem  33235  domnprodn0  33369  rprmdvdsprod  33627  zringfrac  33647  ply1coedeg  33682  extvfvvcl  33712  extvfvcl  33713  evlextv  33719  psrmonprod  33729  esplyind  33752  esplyindfv  33753  esplyfvn  33754  vieta  33757  lindsunlem  33802  dimkerim  33805  madjusmdetlem1  34005  ist0cld  34011  esumpad  34233  esumpad2  34234  measiun  34396  difelcarsg  34488  carsgclctunlem2  34497  tgoldbachgtde  34838  f1resrcmplf1d  35264  satfv1lem  35578  dmopab3rexdif  35621  mthmpps  35798  dvreasin  37957  dvreacos  37958  areacirclem4  37962  sticksstones22  42538  selvvvval  42943  evlselvlem  42944  evlselv  42945  ntrclsrcomplex  44391  ntrclsfveq1  44416  ntrclsiso  44423  ntrclsk2  44424  ntrclskb  44425  ntrclsk3  44426  ntrclsk13  44427  ntrneircomplex  44430  clsneircomplex  44459  clsneiel1  44464  neicvgrcomplex  44469  neicvgel1  44475  difmap  45565  difmapsn  45570  supminfxr2  45827  iccdifprioo  45876  limciccioolb  45981  lptioo2  45991  lptioo1  45992  limcicciooub  45995  dvdivcncf  46285  itgvol0  46326  itgcoscmulx  46327  itgsincmulx  46332  ismbl3  46344  stoweidlem28  46386  stoweidlem50  46408  dirkeritg  46460  dirkercncflem2  46462  dirkercncflem4  46464  fourierdlem39  46504  fourierdlem58  46522  fourierdlem68  46532  fourierdlem76  46540  fourierdlem102  46566  fourierdlem114  46578  pwsal  46673  salexct  46692  sge0fodjrnlem  46774  iundjiun  46818  meaunle  46822  meadjiunlem  46823  meaiunlelem  46826  meadif  46837  meaiuninclem  46838  meaiininclem  46844  carageniuncllem2  46880  caragencmpl  46893  hsphoidmvle2  46943  hsphoidmvle  46944  hoidmv1lelem2  46950  hspmbllem1  46984  hspmbllem3  46986  uhgrimisgrgric  48291  fdmdifeqresdif  48702  lincdifsn  48784  lincresunit2  48838  lincresunit3lem2  48840  iscnrm3rlem3  49301  iscnrm3rlem7  49305