Theorem difssd 4109

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3933   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-dif 3939  df-in 3943  df-ss 3952

This theorem is referenced by:  uneqdifeq  4438  fofinf1o  8793  ackbij1lem12  9647  ssfin4  9726  enfin1ai  9800  fpwwe2  10059  wundif  10130  cshimadifsn  14185  fprodn0f  15339  rpnnen2lem11  15571  mrieqvlemd  16894  mrieqv2d  16904  symgextfo  18544  symgextres  18547  symgfixelsi  18557  pmtrdifellem1  18598  pmtrdifellem2  18599  dprdfeq0  19138  dpjf  19173  dpjlid  19177  dpjghm  19179  ablfac1eu  19189  subdrgint  19576  islbs3  19921  lbsextlem4  19927  frlmsslss2  20913  frlmlbs  20935  mdetrlin  21205  mdetrsca  21206  mdetralt  21211  mdetmul  21226  smadiadetlem3lem0  21268  smadiadet  21273  clsval2  21652  hausllycmp  22096  qtoprest  22319  trfil3  22490  ufileu  22521  fclscf  22627  alexsublem  22646  blcld  23109  restmetu  23174  evth  23557  lebnumlem1  23559  lebnumlem2  23560  lebnumlem3  23561  cmmbl  24129  nulmbl2  24131  volinun  24141  volsup  24151  uniioombllem3  24180  uniioombllem5  24182  uniioombl  24184  itg1addlem5  24295  itg2cnlem2  24357  dvreslem  24501  dvres2lem  24502  dvaddbr  24529  dvmulbr  24530  dvrec  24546  dvexp3  24569  dveflem  24570  dvcnvrelem2  24609  uhgrspan1  27079  unidifsnel  30289  fprodeq02  30534  symgcom2  30723  cycpmconjvlem  30778  lindsunlem  31015  dimkerim  31018  madjusmdetlem1  31087  indsum  31275  indsumin  31276  esumpad  31309  esumpad2  31310  measiun  31472  difelcarsg  31563  carsgclctunlem2  31572  tgoldbachgtde  31926  f1resrcmplf1d  32355  satfv1lem  32604  dmopab3rexdif  32647  mthmpps  32824  fpr1  33134  dvreasin  34974  dvreacos  34975  areacirclem4  34979  ntrclsrcomplex  40378  ntrclsfveq1  40403  ntrclsiso  40410  ntrclsk2  40411  ntrclskb  40412  ntrclsk3  40413  ntrclsk13  40414  ntrneircomplex  40417  clsneircomplex  40446  clsneiel1  40451  neicvgrcomplex  40456  neicvgel1  40462  difmap  41462  difmapsn  41467  supminfxr2  41737  iccdifprioo  41784  limciccioolb  41894  lptioo2  41904  lptioo1  41905  limcicciooub  41910  dvdivcncf  42204  itgvol0  42245  itgcoscmulx  42246  itgsincmulx  42251  ismbl3  42264  stoweidlem28  42306  stoweidlem50  42328  dirkeritg  42380  dirkercncflem2  42382  dirkercncflem4  42384  fourierdlem39  42424  fourierdlem58  42442  fourierdlem68  42452  fourierdlem76  42460  fourierdlem102  42486  fourierdlem114  42498  pwsal  42593  salexct  42610  sge0fodjrnlem  42691  iundjiun  42735  meaunle  42739  meadjiunlem  42740  meaiunlelem  42743  meadif  42754  meaiuninclem  42755  meaiininclem  42761  carageniuncllem2  42797  caragencmpl  42810  hsphoidmvle2  42860  hsphoidmvle  42861  hoidmv1lelem2  42867  hspmbllem1  42901  hspmbllem3  42903  fdmdifeqresdif  44383  lincdifsn  44472  lincresunit2  44526  lincresunit3lem2  44528