MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difssd Unicode version

Theorem difssd 3631
Description: A difference of two classes is contained in the minuend. Deduction form of difss 3630. (Contributed by David Moews, 1-May-2017.)
Assertion
Ref Expression
difssd

Proof of Theorem difssd
StepHypRef Expression
1 difss 3630 . 2
21a1i 11 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \cdif 3472  C_wss 3475
This theorem is referenced by:  fofinf1o  7821  ackbij1lem12  8632  ssfin4  8711  enfin1ai  8785  fpwwe2  9042  wundif  9113  rpnnen2lem11  13958  mrieqvlemd  15026  mrieqv2d  15036  symgextfo  16447  symgextres  16450  symgfixelsi  16460  pmtrdifellem1  16501  pmtrdifellem2  16502  dprdfeq0  17062  dprdfeq0OLD  17069  dpjf  17106  dpjlid  17110  dpjghm  17112  ablfac1eu  17124  islbs3  17801  lbsextlem4  17807  frlmsslss2  18805  frlmsslss2OLD  18806  frlmlbs  18831  mdetrlin  19104  mdetrsca  19105  mdetralt  19110  mdetmul  19125  smadiadetlem3lem0  19167  smadiadet  19172  clsval2  19551  hausllycmp  19995  qtoprest  20218  trfil3  20389  ufileu  20420  fclscf  20526  alexsublem  20544  blcld  21008  restmetu  21090  evth  21459  lebnumlem1  21461  lebnumlem2  21462  lebnumlem3  21463  cmmbl  21945  nulmbl2  21947  volinun  21956  volsup  21966  uniioombllem3  21994  uniioombllem5  21996  uniioombl  21998  itg1addlem5  22107  itg2cnlem2  22169  dvreslem  22313  dvres2lem  22314  dvaddbr  22341  dvmulbr  22342  dvrec  22358  dvexp3  22379  dveflem  22380  dvcnvrelem2  22419  indsum  28036  measiun  28189  mthmpps  28942  dvreasin  30105  dvreacos  30106  areacirclem4  30110  iccdifprioo  31556  fprodn0f  31594  limciccioolb  31627  lptioo2  31637  lptioo1  31638  limcicciooub  31643  dvdivcncf  31724  itgvol0  31767  itgcoscmulx  31768  itgsincmulx  31773  stoweidlem28  31810  stoweidlem50  31832  dirkeritg  31884  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem39  31928  fourierdlem58  31947  fourierdlem68  31957  fourierdlem76  31965  fourierdlem102  31991  fourierdlem114  32003  fdmdifeqresdif  32931  lincdifsn  33025  lincresunit2  33079  lincresunit3lem2  33081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator