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

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

Proof of Theorem difssd
StepHypRef Expression
1 difss 3480 . 2  |-  ( A 
\  B )  C_  A
21a1i 11 1  |-  ( ph  ->  ( A  \  B
)  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \ cdif 3322    C_ wss 3325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-dif 3328  df-in 3332  df-ss 3339
This theorem is referenced by:  fofinf1o  7588  ackbij1lem12  8396  ssfin4  8475  enfin1ai  8549  fpwwe2  8806  wundif  8877  rpnnen2lem11  13503  mrieqvlemd  14563  mrieqv2d  14573  symgextfo  15920  symgextres  15923  symgfixelsi  15933  pmtrdifellem1  15975  pmtrdifellem2  15976  dprdfeq0  16502  dprdfeq0OLD  16509  dpjf  16546  dpjlid  16550  dpjghm  16552  ablfac1eu  16564  islbs3  17214  lbsextlem4  17220  frlmsslss2  18158  frlmsslss2OLD  18159  frlmlbs  18184  mdetrlin  18368  mdetrsca  18369  mdetralt  18373  mdetmul  18388  smadiadetlem3lem0  18430  smadiadet  18435  clsval2  18613  hausllycmp  19057  qtoprest  19249  trfil3  19420  ufileu  19451  fclscf  19557  alexsublem  19575  blcld  20039  restmetu  20121  evth  20490  lebnumlem1  20492  lebnumlem2  20493  lebnumlem3  20494  cmmbl  20975  nulmbl2  20977  volinun  20986  volsup  20996  uniioombllem3  21024  uniioombllem5  21026  uniioombl  21028  itg1addlem5  21137  itg2cnlem2  21199  dvreslem  21343  dvres2lem  21344  dvaddbr  21371  dvmulbr  21372  dvrec  21388  dvexp3  21409  dveflem  21410  dvcnvrelem2  21449  ofpreima2  25920  indsum  26415  measiun  26568  dvreasin  28407  dvreacos  28408  areacirclem4  28412  stoweidlem28  29748  stoweidlem50  29770  fdmdifeqresdif  30656  lincdifsn  30799  lincresunit2  30853  lincresunit3lem2  30855
  Copyright terms: Public domain W3C validator