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

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

Proof of Theorem difssd
StepHypRef Expression
1 difss 3483 . 2  |-  ( A 
\  B )  C_  A
21a1i 11 1  |-  ( ph  ->  ( A  \  B
)  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \ cdif 3325    C_ wss 3328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2974  df-dif 3331  df-in 3335  df-ss 3342
This theorem is referenced by:  fofinf1o  7592  ackbij1lem12  8400  ssfin4  8479  enfin1ai  8553  fpwwe2  8810  wundif  8881  rpnnen2lem11  13507  mrieqvlemd  14567  mrieqv2d  14577  symgextfo  15927  symgextres  15930  symgfixelsi  15940  pmtrdifellem1  15982  pmtrdifellem2  15983  dprdfeq0  16512  dprdfeq0OLD  16519  dpjf  16556  dpjlid  16560  dpjghm  16562  ablfac1eu  16574  islbs3  17236  lbsextlem4  17242  frlmsslss2  18199  frlmsslss2OLD  18200  frlmlbs  18225  mdetrlin  18409  mdetrsca  18410  mdetralt  18414  mdetmul  18429  smadiadetlem3lem0  18471  smadiadet  18476  clsval2  18654  hausllycmp  19098  qtoprest  19290  trfil3  19461  ufileu  19492  fclscf  19598  alexsublem  19616  blcld  20080  restmetu  20162  evth  20531  lebnumlem1  20533  lebnumlem2  20534  lebnumlem3  20535  cmmbl  21016  nulmbl2  21018  volinun  21027  volsup  21037  uniioombllem3  21065  uniioombllem5  21067  uniioombl  21069  itg1addlem5  21178  itg2cnlem2  21240  dvreslem  21384  dvres2lem  21385  dvaddbr  21412  dvmulbr  21413  dvrec  21429  dvexp3  21450  dveflem  21451  dvcnvrelem2  21490  ofpreima2  25985  indsum  26479  measiun  26632  dvreasin  28482  dvreacos  28483  areacirclem4  28487  stoweidlem28  29823  stoweidlem50  29845  fdmdifeqresdif  30732  lincdifsn  30958  lincresunit2  31012  lincresunit3lem2  31014
  Copyright terms: Public domain W3C validator