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

Theorem eldifbd 3325
Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3322. (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 3322 . . 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 1725    \ cdif 3309
This theorem is referenced by:  boxcutc  7097  infeq5i  7583  cantnflem2  7638  ackbij1lem18  8109  infpssrlem4  8178  fin23lem30  8214  domtriomlem  8314  pwfseqlem4  8529  dprdfadd  15570  pgpfac1lem2  15625  pgpfac1lem3a  15626  pgpfac1lem3  15627  lspsolv  16207  lsppratlem3  16213  mplsubrglem  16494  hauscmplem  17461  1stccnp  17517  1stckgen  17578  alexsublem  18067  bcthlem4  19272  plyeq0lem  20121  ftalem3  20849  qqhval2  24358  sibfof  24646  rmspecnonsq  26961  frlmssuvc2  27215  stoweidlem43  27759  dochnel2  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-dif 3315
  Copyright terms: Public domain W3C validator