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

Theorem eldifbd 3362
Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3359. (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 3359 . . 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 3346
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 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-dif 3352
This theorem is referenced by:  xpdifid  5287  boxcutc  7327  infeq5i  7863  cantnflem2  7919  ackbij1lem18  8427  infpssrlem4  8496  fin23lem30  8532  domtriomlem  8632  pwfseqlem4  8850  dprdfadd  16532  dprdfaddOLD  16539  pgpfac1lem2  16598  pgpfac1lem3a  16599  pgpfac1lem3  16600  lspsolv  17246  lsppratlem3  17252  mplsubrglem  17539  mplsubrglemOLD  17540  frlmssuvc2  18242  frlmssuvc2OLD  18244  hauscmplem  19031  1stccnp  19088  1stckgen  19149  alexsublem  19638  bcthlem4  20860  plyeq0lem  21700  ftalem3  22434  tglngne  23006  ofpreima2  26007  qqhval2  26433  sibfof  26748  eulerpartlemsv2  26763  eulerpartlemv  26769  eulerpartlemgs2  26785  rmspecnonsq  29274  stoweidlem43  29864  dochnel2  35133
  Copyright terms: Public domain W3C validator