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

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

Proof of Theorem difssd
StepHypRef Expression
1 difss 3466 . 2  |-  ( A 
\  B )  C_  A
21a1i 11 1  |-  ( ph  ->  ( A  \  B
)  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \ cdif 3309    C_ wss 3312
This theorem is referenced by:  fofinf1o  7378  ackbij1lem12  8100  ssfin4  8179  enfin1ai  8253  fpwwe2  8507  wundif  8578  rpnnen2lem11  12812  mrieqvlemd  13842  mrieqv2d  13852  dprdfeq0  15568  dpjf  15603  dpjlid  15607  dpjghm  15609  ablfac1eu  15619  islbs3  16215  lbsextlem4  16221  clsval2  17102  hausllycmp  17545  qtoprest  17737  trfil3  17908  ufileu  17939  fclscf  18045  alexsublem  18063  blcld  18523  restmetu  18605  evth  18972  lebnumlem1  18974  lebnumlem2  18975  lebnumlem3  18976  cmmbl  19417  nulmbl2  19419  volinun  19428  volsup  19438  uniioombllem3  19465  uniioombllem5  19467  uniioombl  19469  itg1addlem5  19580  itg2cnlem2  19642  dvreslem  19784  dvres2lem  19785  dvaddbr  19812  dvmulbr  19813  dvrec  19829  dvexp3  19850  dveflem  19851  dvcnvrelem2  19890  indsum  24408  measiun  24560  sibfof  24642  areacirclem5  26232  frlmsslss2  27160  frlmlbs  27164  stoweidlem28  27691  stoweidlem50  27713
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-dif 3315  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator