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

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

Proof of Theorem difssd
StepHypRef Expression
1 difss 3631 . 2  |-  ( A 
\  B )  C_  A
21a1i 11 1  |-  ( ph  ->  ( A  \  B
)  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \ cdif 3473    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490
This theorem is referenced by:  fofinf1o  7800  ackbij1lem12  8610  ssfin4  8689  enfin1ai  8763  fpwwe2  9020  wundif  9091  rpnnen2lem11  13818  mrieqvlemd  14883  mrieqv2d  14893  symgextfo  16249  symgextres  16252  symgfixelsi  16262  pmtrdifellem1  16304  pmtrdifellem2  16305  dprdfeq0  16861  dprdfeq0OLD  16868  dpjf  16905  dpjlid  16909  dpjghm  16911  ablfac1eu  16923  islbs3  17596  lbsextlem4  17602  frlmsslss2  18588  frlmsslss2OLD  18589  frlmlbs  18614  mdetrlin  18887  mdetrsca  18888  mdetralt  18893  mdetmul  18908  smadiadetlem3lem0  18950  smadiadet  18955  clsval2  19333  hausllycmp  19777  qtoprest  19969  trfil3  20140  ufileu  20171  fclscf  20277  alexsublem  20295  blcld  20759  restmetu  20841  evth  21210  lebnumlem1  21212  lebnumlem2  21213  lebnumlem3  21214  cmmbl  21696  nulmbl2  21698  volinun  21707  volsup  21717  uniioombllem3  21745  uniioombllem5  21747  uniioombl  21749  itg1addlem5  21858  itg2cnlem2  21920  dvreslem  22064  dvres2lem  22065  dvaddbr  22092  dvmulbr  22093  dvrec  22109  dvexp3  22130  dveflem  22131  dvcnvrelem2  22170  ofpreima2  27196  indsum  27692  measiun  27845  dvreasin  29698  dvreacos  29699  areacirclem4  29703  iccdifprioo  31136  limciccioolb  31179  lptioo2  31189  lptioo1  31190  limcicciooub  31195  cncficcgt0  31243  dvdivcncf  31273  itgvol0  31302  itgcoscmulx  31303  itgsincmulx  31308  stoweidlem28  31344  stoweidlem50  31366  dirkeritg  31418  dirkercncflem2  31420  dirkercncflem4  31422  fourierdlem39  31462  fourierdlem58  31481  fourierdlem68  31491  fourierdlem76  31499  fourierdlem102  31525  fourierdlem114  31537  fdmdifeqresdif  32015  lincdifsn  32115  lincresunit2  32169  lincresunit3lem2  32171
  Copyright terms: Public domain W3C validator