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

Theorem eldifbd 3489
Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3486. (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 3486 . . 3  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
31, 2sylib 196 . 2  |-  ( ph  ->  ( A  e.  B  /\  -.  A  e.  C
) )
43simprd 463 1  |-  ( ph  ->  -.  A  e.  C
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    e. wcel 1767    \ cdif 3473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479
This theorem is referenced by:  xpdifid  5435  boxcutc  7513  infeq5i  8054  cantnflem2  8110  ackbij1lem18  8618  infpssrlem4  8687  fin23lem30  8723  domtriomlem  8823  pwfseqlem4  9041  dprdfadd  16874  dprdfaddOLD  16881  pgpfac1lem2  16940  pgpfac1lem3a  16941  pgpfac1lem3  16942  lspsolv  17601  lsppratlem3  17607  mplsubrglem  17911  mplsubrglemOLD  17912  frlmssuvc2  18633  frlmssuvc2OLD  18635  hauscmplem  19712  1stccnp  19769  1stckgen  19882  alexsublem  20371  bcthlem4  21593  plyeq0lem  22434  ftalem3  23173  tglngne  23762  ofpreima2  27277  qqhval2  27714  sibfof  28033  eulerpartlemsv2  28048  eulerpartlemv  28054  eulerpartlemgs2  28070  rmspecnonsq  30674  dstregt0  31267  lptre2pt  31409  stoweidlem43  31570  fourierdlem66  31700  dochnel2  36406
  Copyright terms: Public domain W3C validator