Theorem difssd 4099

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

Assertion

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

Proof of Theorem difssd

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

Syntax hints:   → wi 4   ∖ cdif 3910   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-ss 3930

This theorem is referenced by:  uneqdifeq  4458  fpr1  8300  fofinf1o  9289  ackbij1lem12  10213  ssfin4  10294  enfin1ai  10368  fpwwe2  10628  wundif  10699  cshimadifsn  14866  indsum  15880  fprodn0f  16045  rpnnen2lem11  16280  mrieqvlemd  17685  mrieqv2d  17695  symgextfo  19492  symgextres  19495  symgfixelsi  19505  pmtrdifellem1  19546  pmtrdifellem2  19547  dprdfeq0  20094  dpjf  20129  dpjlid  20133  dpjghm  20135  ablfac1eu  20145  subdrgint  20884  islbs3  21257  lbsextlem4  21263  cnflddiv  21521  frlmsslss2  21894  frlmlbs  21916  selvvvval  22262  psdmul  22298  mdetrlin  22728  mdetrsca  22729  mdetralt  22734  mdetmul  22749  smadiadetlem3lem0  22791  smadiadet  22796  clsval2  23176  hausllycmp  23620  qtoprest  23843  trfil3  24014  ufileu  24045  fclscf  24151  alexsublem  24170  blcld  24631  restmetu  24696  evth  25087  lebnumlem1  25089  lebnumlem2  25090  lebnumlem3  25091  cmmbl  25662  nulmbl2  25664  volinun  25674  volsup  25684  uniioombllem3  25713  uniioombllem5  25715  uniioombl  25717  itg1addlem5  25828  itg2cnlem2  25890  dvreslem  26037  dvres2lem  26038  dvaddbr  26066  dvmulbr  26067  dvrec  26083  dvexp3  26106  dveflem  26107  dvcnvrelem2  26146  uhgrspan1  29594  unidifsnel  32822  fdifsupp  32971  fdifsuppconst  32975  fmptunsnop  32986  fprodeq02  33109  indsumin  33122  gsumhashmul  33328  suppgsumssiun  33333  symgcom2  33345  cycpmconjvlem  33402  domnprodn0  33539  dflringlem2  33730  rprmdvdsprod  33769  zringfrac  33789  ply1coedeg  33824  selvascl  33852  selvply1rhm0  33861  extvfvvcl  33870  extvfvcl  33871  evlextv  33877  psrmonprod  33887  esplyind  33910  esplyindfv  33911  esplyfvn  33912  vieta  33915  lindsunlem  33959  dimkerim  33962  madjusmdetlem1  34162  ist0cld  34168  esumpad  34390  esumpad2  34391  measiun  34553  difelcarsg  34645  carsgclctunlem2  34654  tgoldbachgtde  34992  f1resrcmplf1d  35419  satfv1lem  35753  dmopab3rexdif  35796  mthmpps  35973  dvreasin  38245  dvreacos  38246  areacirclem4  38250  sticksstones22  42825  evlselvlem  43212  evlselv  43213  ntrclsrcomplex  44653  ntrclsfveq1  44678  ntrclsiso  44685  ntrclsk2  44686  ntrclskb  44687  ntrclsk3  44688  ntrclsk13  44689  ntrneircomplex  44692  clsneircomplex  44721  clsneiel1  44726  neicvgrcomplex  44731  neicvgel1  44737  difmap  45815  difmapsn  45820  supminfxr2  46075  iccdifprioo  46124  limciccioolb  46229  lptioo2  46239  lptioo1  46240  limcicciooub  46243  dvdivcncf  46533  itgvol0  46574  itgcoscmulx  46575  itgsincmulx  46580  ismbl3  46592  stoweidlem28  46634  stoweidlem50  46656  dirkeritg  46708  dirkercncflem2  46710  dirkercncflem4  46712  fourierdlem39  46752  fourierdlem58  46770  fourierdlem68  46780  fourierdlem76  46788  fourierdlem102  46814  fourierdlem114  46826  pwsal  46921  salexct  46940  sge0fodjrnlem  47022  iundjiun  47066  meaunle  47070  meadjiunlem  47071  meaiunlelem  47074  meadif  47085  meaiuninclem  47086  meaiininclem  47092  carageniuncllem2  47128  caragencmpl  47141  hsphoidmvle2  47191  hsphoidmvle  47192  hoidmv1lelem2  47198  hspmbllem1  47232  hspmbllem3  47234  uhgrimisgrgric  48585  fdmdifeqresdif  49007  lincdifsn  49089  lincresunit2  49143  lincresunit3lem2  49145  iscnrm3rlem3  49605  iscnrm3rlem7  49609