Theorem difssd 4077

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3886   ⊆ wss 3889

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-ss 3906

This theorem is referenced by:  uneqdifeq  4432  fpr1  8253  fofinf1o  9242  ackbij1lem12  10152  ssfin4  10232  enfin1ai  10306  fpwwe2  10566  wundif  10637  cshimadifsn  14791  indsum  15791  fprodn0f  15956  rpnnen2lem11  16191  mrieqvlemd  17595  mrieqv2d  17605  symgextfo  19397  symgextres  19400  symgfixelsi  19410  pmtrdifellem1  19451  pmtrdifellem2  19452  dprdfeq0  19999  dpjf  20034  dpjlid  20038  dpjghm  20040  ablfac1eu  20050  subdrgint  20780  islbs3  21153  lbsextlem4  21159  cnflddiv  21382  frlmsslss2  21755  frlmlbs  21777  psdmul  22132  mdetrlin  22567  mdetrsca  22568  mdetralt  22573  mdetmul  22588  smadiadetlem3lem0  22630  smadiadet  22635  clsval2  23015  hausllycmp  23459  qtoprest  23682  trfil3  23853  ufileu  23884  fclscf  23990  alexsublem  24009  blcld  24470  restmetu  24535  evth  24926  lebnumlem1  24928  lebnumlem2  24929  lebnumlem3  24930  cmmbl  25501  nulmbl2  25503  volinun  25513  volsup  25523  uniioombllem3  25552  uniioombllem5  25554  uniioombl  25556  itg1addlem5  25667  itg2cnlem2  25729  dvreslem  25876  dvres2lem  25877  dvaddbr  25905  dvmulbr  25906  dvrec  25922  dvexp3  25945  dveflem  25946  dvcnvrelem2  25985  uhgrspan1  29372  unidifsnel  32605  fdifsupp  32758  fdifsuppconst  32762  fmptunsnop  32773  fprodeq02  32897  indsumin  32921  gsumhashmul  33128  suppgsumssiun  33133  symgcom2  33145  cycpmconjvlem  33202  domnprodn0  33336  rprmdvdsprod  33594  zringfrac  33614  ply1coedeg  33649  extvfvvcl  33679  extvfvcl  33680  evlextv  33686  psrmonprod  33696  esplyind  33719  esplyindfv  33720  esplyfvn  33721  vieta  33724  lindsunlem  33768  dimkerim  33771  madjusmdetlem1  33971  ist0cld  33977  esumpad  34199  esumpad2  34200  measiun  34362  difelcarsg  34454  carsgclctunlem2  34463  tgoldbachgtde  34804  f1resrcmplf1d  35230  satfv1lem  35544  dmopab3rexdif  35587  mthmpps  35764  dvreasin  38027  dvreacos  38028  areacirclem4  38032  sticksstones22  42607  selvvvval  43018  evlselvlem  43019  evlselv  43020  ntrclsrcomplex  44462  ntrclsfveq1  44487  ntrclsiso  44494  ntrclsk2  44495  ntrclskb  44496  ntrclsk3  44497  ntrclsk13  44498  ntrneircomplex  44501  clsneircomplex  44530  clsneiel1  44535  neicvgrcomplex  44540  neicvgel1  44546  difmap  45636  difmapsn  45641  supminfxr2  45897  iccdifprioo  45946  limciccioolb  46051  lptioo2  46061  lptioo1  46062  limcicciooub  46065  dvdivcncf  46355  itgvol0  46396  itgcoscmulx  46397  itgsincmulx  46402  ismbl3  46414  stoweidlem28  46456  stoweidlem50  46478  dirkeritg  46530  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem39  46574  fourierdlem58  46592  fourierdlem68  46602  fourierdlem76  46610  fourierdlem102  46636  fourierdlem114  46648  pwsal  46743  salexct  46762  sge0fodjrnlem  46844  iundjiun  46888  meaunle  46892  meadjiunlem  46893  meaiunlelem  46896  meadif  46907  meaiuninclem  46908  meaiininclem  46914  carageniuncllem2  46950  caragencmpl  46963  hsphoidmvle2  47013  hsphoidmvle  47014  hoidmv1lelem2  47020  hspmbllem1  47054  hspmbllem3  47056  uhgrimisgrgric  48407  fdmdifeqresdif  48818  lincdifsn  48900  lincresunit2  48954  lincresunit3lem2  48956  iscnrm3rlem3  49417  iscnrm3rlem7  49421