Theorem difssd 4025

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3851   ⊆ wss 3854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-v 3434  df-dif 3857  df-in 3861  df-ss 3869

This theorem is referenced by:  uneqdifeq  4346  fofinf1o  8635  ackbij1lem12  9488  ssfin4  9567  enfin1ai  9641  fpwwe2  9900  wundif  9971  cshimadifsn  14015  fprodn0f  15166  rpnnen2lem11  15398  mrieqvlemd  16717  mrieqv2d  16727  symgextfo  18269  symgextres  18272  symgfixelsi  18282  pmtrdifellem1  18323  pmtrdifellem2  18324  dprdfeq0  18849  dpjf  18884  dpjlid  18888  dpjghm  18890  ablfac1eu  18900  subdrgint  19260  islbs3  19605  lbsextlem4  19611  frlmsslss2  20589  frlmlbs  20611  mdetrlin  20883  mdetrsca  20884  mdetralt  20889  mdetmul  20904  smadiadetlem3lem0  20946  smadiadet  20951  clsval2  21330  hausllycmp  21774  qtoprest  21997  trfil3  22168  ufileu  22199  fclscf  22305  alexsublem  22324  blcld  22786  restmetu  22851  evth  23234  lebnumlem1  23236  lebnumlem2  23237  lebnumlem3  23238  cmmbl  23806  nulmbl2  23808  volinun  23818  volsup  23828  uniioombllem3  23857  uniioombllem5  23859  uniioombl  23861  itg1addlem5  23972  itg2cnlem2  24034  dvreslem  24178  dvres2lem  24179  dvaddbr  24206  dvmulbr  24207  dvrec  24223  dvexp3  24246  dveflem  24247  dvcnvrelem2  24286  uhgrspan1  26756  unidifsnel  29963  fprodeq02  30194  cycpmconjvlem  30383  lindsunlem  30579  dimkerim  30582  madjusmdetlem1  30663  indsum  30853  indsumin  30854  esumpad  30887  esumpad2  30888  measiun  31050  difelcarsg  31141  carsgclctunlem2  31150  tgoldbachgtde  31504  f1resrcmplf1d  31930  dmopab3rexdif  32213  mthmpps  32382  fpr1  32693  dvreasin  34457  dvreacos  34458  areacirclem4  34462  ntrclsrcomplex  39821  ntrclsfveq1  39846  ntrclsiso  39853  ntrclsk2  39854  ntrclskb  39855  ntrclsk3  39856  ntrclsk13  39857  ntrneircomplex  39860  clsneircomplex  39889  clsneiel1  39894  neicvgrcomplex  39899  neicvgel1  39905  difmap  40963  difmapsn  40968  supminfxr2  41241  iccdifprioo  41288  limciccioolb  41398  lptioo2  41408  lptioo1  41409  limcicciooub  41414  dvdivcncf  41707  itgvol0  41748  itgcoscmulx  41749  itgsincmulx  41754  ismbl3  41767  stoweidlem28  41809  stoweidlem50  41831  dirkeritg  41883  dirkercncflem2  41885  dirkercncflem4  41887  fourierdlem39  41927  fourierdlem58  41945  fourierdlem68  41955  fourierdlem76  41963  fourierdlem102  41989  fourierdlem114  42001  pwsal  42096  salexct  42113  sge0fodjrnlem  42194  iundjiun  42238  meaunle  42242  meadjiunlem  42243  meaiunlelem  42246  meadif  42257  meaiuninclem  42258  meaiininclem  42264  carageniuncllem2  42300  caragencmpl  42313  hsphoidmvle2  42363  hsphoidmvle  42364  hoidmv1lelem2  42370  hspmbllem1  42404  hspmbllem3  42406  fdmdifeqresdif  43822  lincdifsn  43913  lincresunit2  43967  lincresunit3lem2  43969