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

Theorem difss2d 3469
 Description: If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3468. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
difss2d.1
Assertion
Ref Expression
difss2d

Proof of Theorem difss2d
StepHypRef Expression
1 difss2d.1 . 2
2 difss2 3468 . 2
31, 2syl 16 1
 Colors of variables: wff set class Syntax hints:   wi 4   cdif 3309   wss 3312 This theorem is referenced by:  oacomf1olem  6799  numacn  7922  ramub1lem1  13386  ramub1lem2  13387  mreexexlem2d  13862  mreexexlem3d  13863  mreexexlem4d  13864  mreexexd  13865  acsfiindd  14595  dpjidcl  15608  clsval2  17106  llycmpkgen2  17574  1stckgen  17578  alexsublem  18067  bcthlem3  19271  neibastop2lem  26380  eldioph2lem2  26810 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