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

Theorem eldifd 3249
Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3248. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
eldifd.1  |-  ( ph  ->  A  e.  B )
eldifd.2  |-  ( ph  ->  -.  A  e.  C
)
Assertion
Ref Expression
eldifd  |-  ( ph  ->  A  e.  ( B 
\  C ) )

Proof of Theorem eldifd
StepHypRef Expression
1 eldifd.1 . 2  |-  ( ph  ->  A  e.  B )
2 eldifd.2 . 2  |-  ( ph  ->  -.  A  e.  C
)
3 eldif 3248 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
41, 2, 3sylanbrc 645 1  |-  ( ph  ->  A  e.  ( B 
\  C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1715    \ cdif 3235
This theorem is referenced by:  incexclem  12503  mreexd  13754  elzrhunit  23835  qqhval2  23838  prodrblem  24739  fprodcvg  24740  fprodss  24758  rpdmgamma  24833  dvreasin  25698  areacirclem5  25704  climrec  27235  wallispi  27325  nbcusgra  27628  usgrasscusgra  27648  uvtxnbgra  27658  frgrancvvdeqlem1  27865  frgrawopreglem4  27882
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-dif 3241
  Copyright terms: Public domain W3C validator