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

Theorem eldifbd 3277
Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3274. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
eldifbd.1  |-  ( ph  ->  A  e.  ( B 
\  C ) )
Assertion
Ref Expression
eldifbd  |-  ( ph  ->  -.  A  e.  C
)

Proof of Theorem eldifbd
StepHypRef Expression
1 eldifbd.1 . . 3  |-  ( ph  ->  A  e.  ( B 
\  C ) )
2 eldif 3274 . . 3  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
31, 2sylib 189 . 2  |-  ( ph  ->  ( A  e.  B  /\  -.  A  e.  C
) )
43simprd 450 1  |-  ( ph  ->  -.  A  e.  C
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359    e. wcel 1717    \ cdif 3261
This theorem is referenced by:  boxcutc  7042  infeq5i  7525  cantnflem2  7580  ackbij1lem18  8051  infpssrlem4  8120  fin23lem30  8156  domtriomlem  8256  pwfseqlem4  8471  dprdfadd  15506  pgpfac1lem2  15561  pgpfac1lem3a  15562  pgpfac1lem3  15563  lspsolv  16143  lsppratlem3  16149  mplsubrglem  16430  hauscmplem  17392  1stccnp  17447  1stckgen  17508  alexsublem  17997  bcthlem4  19150  plyeq0lem  19997  ftalem3  20725  qqhval2  24166  rmspecnonsq  26662  frlmssuvc2  26917  stoweidlem43  27461  dochnel2  31508
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-dif 3267
  Copyright terms: Public domain W3C validator