Theorem difssd 4132

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3945   ⊆ wss 3948

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 3951  df-in 3955  df-ss 3965

This theorem is referenced by:  uneqdifeq  4492  fpr1  8285  fofinf1o  9324  ackbij1lem12  10223  ssfin4  10302  enfin1ai  10376  fpwwe2  10635  wundif  10706  cshimadifsn  14777  fprodn0f  15932  rpnnen2lem11  16164  mrieqvlemd  17570  mrieqv2d  17580  symgextfo  19285  symgextres  19288  symgfixelsi  19298  pmtrdifellem1  19339  pmtrdifellem2  19340  dprdfeq0  19887  dpjf  19922  dpjlid  19926  dpjghm  19928  ablfac1eu  19938  subdrgint  20412  islbs3  20761  lbsextlem4  20767  frlmsslss2  21322  frlmlbs  21344  mdetrlin  22096  mdetrsca  22097  mdetralt  22102  mdetmul  22117  smadiadetlem3lem0  22159  smadiadet  22164  clsval2  22546  hausllycmp  22990  qtoprest  23213  trfil3  23384  ufileu  23415  fclscf  23521  alexsublem  23540  blcld  24006  restmetu  24071  evth  24467  lebnumlem1  24469  lebnumlem2  24470  lebnumlem3  24471  cmmbl  25043  nulmbl2  25045  volinun  25055  volsup  25065  uniioombllem3  25094  uniioombllem5  25096  uniioombl  25098  itg1addlem5  25210  itg2cnlem2  25272  dvreslem  25418  dvres2lem  25419  dvaddbr  25447  dvmulbr  25448  dvrec  25464  dvexp3  25487  dveflem  25488  dvcnvrelem2  25527  uhgrspan1  28550  unidifsnel  31760  fdifsuppconst  31899  fprodeq02  32017  gsumhashmul  32196  symgcom2  32233  cycpmconjvlem  32288  lindsunlem  32698  dimkerim  32701  madjusmdetlem1  32796  ist0cld  32802  indsum  33008  indsumin  33009  esumpad  33042  esumpad2  33043  measiun  33205  difelcarsg  33298  carsgclctunlem2  33307  tgoldbachgtde  33661  f1resrcmplf1d  34079  satfv1lem  34342  dmopab3rexdif  34385  mthmpps  34562  gg-dvmulbr  35164  dvreasin  36563  dvreacos  36564  areacirclem4  36568  sticksstones22  40973  selvvvval  41155  evlselvlem  41156  evlselv  41157  ntrclsrcomplex  42772  ntrclsfveq1  42797  ntrclsiso  42804  ntrclsk2  42805  ntrclskb  42806  ntrclsk3  42807  ntrclsk13  42808  ntrneircomplex  42811  clsneircomplex  42840  clsneiel1  42845  neicvgrcomplex  42850  neicvgel1  42856  difmap  43892  difmapsn  43897  supminfxr2  44166  iccdifprioo  44216  limciccioolb  44324  lptioo2  44334  lptioo1  44335  limcicciooub  44340  dvdivcncf  44630  itgvol0  44671  itgcoscmulx  44672  itgsincmulx  44677  ismbl3  44689  stoweidlem28  44731  stoweidlem50  44753  dirkeritg  44805  dirkercncflem2  44807  dirkercncflem4  44809  fourierdlem39  44849  fourierdlem58  44867  fourierdlem68  44877  fourierdlem76  44885  fourierdlem102  44911  fourierdlem114  44923  pwsal  45018  salexct  45037  sge0fodjrnlem  45119  iundjiun  45163  meaunle  45167  meadjiunlem  45168  meaiunlelem  45171  meadif  45182  meaiuninclem  45183  meaiininclem  45189  carageniuncllem2  45225  caragencmpl  45238  hsphoidmvle2  45288  hsphoidmvle  45289  hoidmv1lelem2  45295  hspmbllem1  45329  hspmbllem3  45331  fdmdifeqresdif  46971  lincdifsn  47059  lincresunit2  47113  lincresunit3lem2  47115  iscnrm3rlem3  47529  iscnrm3rlem7  47533