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

Theorem difss2d 4025
Description: If a class is contained in a difference, it is contained in the minuend. Deduction form of difss2 4024. (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 4024 . 2 (𝐴 ⊆ (𝐵𝐶) → 𝐴𝐵)
31, 2syl 17 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3840  wss 3843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-dif 3846  df-in 3850  df-ss 3860
This theorem is referenced by:  oacomf1olem  8223  numacn  9551  ramub1lem1  16464  ramub1lem2  16465  mreexexlem2d  17021  mreexexlem3d  17022  mreexexlem4d  17023  acsfiindd  17905  dpjidcl  19301  clsval2  21803  llycmpkgen2  22303  1stckgen  22307  alexsublem  22797  bcthlem3  24080  pmtrcnelor  30939  lfuhgr  32652  neibastop2lem  34194  pibt2  35233  eldioph2lem2  40177  limccog  42725  fourierdlem56  43267  fourierdlem95  43306
  Copyright terms: Public domain W3C validator