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

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

Proof of Theorem difssd
StepHypRef Expression
1 difss 3476 . 2  |-  ( A 
\  B )  C_  A
21a1i 11 1  |-  ( ph  ->  ( A  \  B
)  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \ cdif 3319    C_ wss 3322
This theorem is referenced by:  fofinf1o  7389  ackbij1lem12  8113  ssfin4  8192  enfin1ai  8266  fpwwe2  8520  wundif  8591  rpnnen2lem11  12826  mrieqvlemd  13856  mrieqv2d  13866  dprdfeq0  15582  dpjf  15617  dpjlid  15621  dpjghm  15623  ablfac1eu  15633  islbs3  16229  lbsextlem4  16235  clsval2  17116  hausllycmp  17559  qtoprest  17751  trfil3  17922  ufileu  17953  fclscf  18059  alexsublem  18077  blcld  18537  restmetu  18619  evth  18986  lebnumlem1  18988  lebnumlem2  18989  lebnumlem3  18990  cmmbl  19431  nulmbl2  19433  volinun  19442  volsup  19452  uniioombllem3  19479  uniioombllem5  19481  uniioombl  19483  itg1addlem5  19594  itg2cnlem2  19656  dvreslem  19798  dvres2lem  19799  dvaddbr  19826  dvmulbr  19827  dvrec  19843  dvexp3  19864  dveflem  19865  dvcnvrelem2  19904  indsum  24422  measiun  24574  sibfof  24656  areacirclem4  26297  frlmsslss2  27224  frlmlbs  27228  stoweidlem28  27755  stoweidlem50  27777
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-dif 3325  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator