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  7390  ackbij1lem12  8116  ssfin4  8195  enfin1ai  8269  fpwwe2  8523  wundif  8594  rpnnen2lem11  12829  mrieqvlemd  13859  mrieqv2d  13869  dprdfeq0  15585  dpjf  15620  dpjlid  15624  dpjghm  15626  ablfac1eu  15636  islbs3  16232  lbsextlem4  16238  clsval2  17119  hausllycmp  17562  qtoprest  17754  trfil3  17925  ufileu  17956  fclscf  18062  alexsublem  18080  blcld  18540  restmetu  18622  evth  18989  lebnumlem1  18991  lebnumlem2  18992  lebnumlem3  18993  cmmbl  19434  nulmbl2  19436  volinun  19445  volsup  19455  uniioombllem3  19482  uniioombllem5  19484  uniioombl  19486  itg1addlem5  19595  itg2cnlem2  19657  dvreslem  19801  dvres2lem  19802  dvaddbr  19829  dvmulbr  19830  dvrec  19846  dvexp3  19867  dveflem  19868  dvcnvrelem2  19907  indsum  24425  measiun  24577  sibfof  24659  areacirclem4  26309  frlmsslss2  27236  frlmlbs  27240  stoweidlem28  27767  stoweidlem50  27789
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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