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

Theorem difss2d 3889
 Description: If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 3888. (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 3888 . 2 (𝐴 ⊆ (𝐵𝐶) → 𝐴𝐵)
31, 2syl 17 1 (𝜑𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∖ cdif 3718   ⊆ wss 3721 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-dif 3724  df-in 3728  df-ss 3735 This theorem is referenced by:  oacomf1olem  7797  numacn  9071  ramub1lem1  15936  ramub1lem2  15937  mreexexlem2d  16512  mreexexlem3d  16513  mreexexlem4d  16514  acsfiindd  17384  dpjidcl  18664  clsval2  21074  llycmpkgen2  21573  1stckgen  21577  alexsublem  22067  bcthlem3  23341  neibastop2lem  32686  eldioph2lem2  37843  limccog  40364  fourierdlem56  40890  fourierdlem95  40929
 Copyright terms: Public domain W3C validator