Theorem difssd 4137

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

Assertion

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

Proof of Theorem difssd

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-ss 3968

This theorem is referenced by:  uneqdifeq  4493  fpr1  8328  fofinf1o  9372  ackbij1lem12  10270  ssfin4  10350  enfin1ai  10424  fpwwe2  10683  wundif  10754  cshimadifsn  14868  fprodn0f  16027  rpnnen2lem11  16260  mrieqvlemd  17672  mrieqv2d  17682  symgextfo  19440  symgextres  19443  symgfixelsi  19453  pmtrdifellem1  19494  pmtrdifellem2  19495  dprdfeq0  20042  dpjf  20077  dpjlid  20081  dpjghm  20083  ablfac1eu  20093  subdrgint  20804  islbs3  21157  lbsextlem4  21163  cnflddiv  21413  frlmsslss2  21795  frlmlbs  21817  psdmul  22170  mdetrlin  22608  mdetrsca  22609  mdetralt  22614  mdetmul  22629  smadiadetlem3lem0  22671  smadiadet  22676  clsval2  23058  hausllycmp  23502  qtoprest  23725  trfil3  23896  ufileu  23927  fclscf  24033  alexsublem  24052  blcld  24518  restmetu  24583  evth  24991  lebnumlem1  24993  lebnumlem2  24994  lebnumlem3  24995  cmmbl  25569  nulmbl2  25571  volinun  25581  volsup  25591  uniioombllem3  25620  uniioombllem5  25622  uniioombl  25624  itg1addlem5  25735  itg2cnlem2  25797  dvreslem  25944  dvres2lem  25945  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvrec  25993  dvexp3  26016  dveflem  26017  dvcnvrelem2  26057  uhgrspan1  29320  unidifsnel  32553  fdifsupp  32694  fdifsuppconst  32698  fmptunsnop  32709  fprodeq02  32825  indsum  32846  indsumin  32847  gsumhashmul  33064  symgcom2  33104  cycpmconjvlem  33161  domnprodn0  33279  rprmdvdsprod  33562  zringfrac  33582  lindsunlem  33675  dimkerim  33678  madjusmdetlem1  33826  ist0cld  33832  esumpad  34056  esumpad2  34057  measiun  34219  difelcarsg  34312  carsgclctunlem2  34321  tgoldbachgtde  34675  f1resrcmplf1d  35101  satfv1lem  35367  dmopab3rexdif  35410  mthmpps  35587  dvreasin  37713  dvreacos  37714  areacirclem4  37718  sticksstones22  42169  selvvvval  42595  evlselvlem  42596  evlselv  42597  ntrclsrcomplex  44048  ntrclsfveq1  44073  ntrclsiso  44080  ntrclsk2  44081  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  ntrneircomplex  44087  clsneircomplex  44116  clsneiel1  44121  neicvgrcomplex  44126  neicvgel1  44132  difmap  45212  difmapsn  45217  supminfxr2  45480  iccdifprioo  45529  limciccioolb  45636  lptioo2  45646  lptioo1  45647  limcicciooub  45652  dvdivcncf  45942  itgvol0  45983  itgcoscmulx  45984  itgsincmulx  45989  ismbl3  46001  stoweidlem28  46043  stoweidlem50  46065  dirkeritg  46117  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem39  46161  fourierdlem58  46179  fourierdlem68  46189  fourierdlem76  46197  fourierdlem102  46223  fourierdlem114  46235  pwsal  46330  salexct  46349  sge0fodjrnlem  46431  iundjiun  46475  meaunle  46479  meadjiunlem  46480  meaiunlelem  46483  meadif  46494  meaiuninclem  46495  meaiininclem  46501  carageniuncllem2  46537  caragencmpl  46550  hsphoidmvle2  46600  hsphoidmvle  46601  hoidmv1lelem2  46607  hspmbllem1  46641  hspmbllem3  46643  uhgrimisgrgric  47899  fdmdifeqresdif  48258  lincdifsn  48341  lincresunit2  48395  lincresunit3lem2  48397  iscnrm3rlem3  48839  iscnrm3rlem7  48843