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

Theorem difss2d 4069
Description: If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 4068. (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 4068 . 2 (𝐴 ⊆ (𝐵𝐶) → 𝐴𝐵)
31, 2syl 17 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3884  wss 3887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904
This theorem is referenced by:  oacomf1olem  8395  numacn  9805  ramub1lem1  16727  ramub1lem2  16728  mreexexlem2d  17354  mreexexlem3d  17355  mreexexlem4d  17356  acsfiindd  18271  dpjidcl  19661  clsval2  22201  llycmpkgen2  22701  1stckgen  22705  alexsublem  23195  bcthlem3  24490  pmtrcnelor  31360  lfuhgr  33079  neibastop2lem  34549  pibt2  35588  eldioph2lem2  40583  limccog  43161  fourierdlem56  43703  fourierdlem95  43742
  Copyright terms: Public domain W3C validator