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

Theorem eldifbd 3334
Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3331. (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 3331 . . 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 1756    \ cdif 3318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2968  df-dif 3324
This theorem is referenced by:  xpdifid  5259  boxcutc  7298  infeq5i  7834  cantnflem2  7890  ackbij1lem18  8398  infpssrlem4  8467  fin23lem30  8503  domtriomlem  8603  pwfseqlem4  8821  dprdfadd  16496  dprdfaddOLD  16503  pgpfac1lem2  16562  pgpfac1lem3a  16563  pgpfac1lem3  16564  lspsolv  17198  lsppratlem3  17204  mplsubrglem  17491  mplsubrglemOLD  17492  frlmssuvc2  18189  frlmssuvc2OLD  18191  hauscmplem  18978  1stccnp  19035  1stckgen  19096  alexsublem  19585  bcthlem4  20807  plyeq0lem  21647  ftalem3  22381  tglngne  22952  ofpreima2  25930  qqhval2  26359  sibfof  26674  eulerpartlemsv2  26689  eulerpartlemv  26695  eulerpartlemgs2  26711  rmspecnonsq  29191  stoweidlem43  29781  dochnel2  34788
  Copyright terms: Public domain W3C validator