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

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

Proof of Theorem difssd
StepHypRef Expression
1 difss 3434 . 2  |-  ( A 
\  B )  C_  A
21a1i 11 1  |-  ( ph  ->  ( A  \  B
)  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \ cdif 3277    C_ wss 3280
This theorem is referenced by:  fofinf1o  7346  ackbij1lem12  8067  ssfin4  8146  enfin1ai  8220  fpwwe2  8474  wundif  8545  rpnnen2lem11  12779  mrieqvlemd  13809  mrieqv2d  13819  dprdfeq0  15535  dpjf  15570  dpjlid  15574  dpjghm  15576  ablfac1eu  15586  islbs3  16182  lbsextlem4  16188  clsval2  17069  hausllycmp  17510  qtoprest  17702  trfil3  17873  ufileu  17904  fclscf  18010  alexsublem  18028  blcld  18488  restmetu  18570  evth  18937  lebnumlem1  18939  lebnumlem2  18940  lebnumlem3  18941  cmmbl  19382  nulmbl2  19384  volinun  19393  volsup  19403  uniioombllem3  19430  uniioombllem5  19432  uniioombl  19434  itg1addlem5  19545  itg2cnlem2  19607  dvreslem  19749  dvres2lem  19750  dvaddbr  19777  dvmulbr  19778  dvrec  19794  dvexp3  19815  dveflem  19816  dvcnvrelem2  19855  indsum  24373  measiun  24525  sibfof  24607  areacirclem5  26185  frlmsslss2  27113  frlmlbs  27117  stoweidlem28  27644  stoweidlem50  27666
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator