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

Theorem eldifbd 3446
Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3443. (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 3443 . . 3  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
31, 2sylib 199 . 2  |-  ( ph  ->  ( A  e.  B  /\  -.  A  e.  C
) )
43simprd 464 1  |-  ( ph  ->  -.  A  e.  C
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 370    e. wcel 1867    \ cdif 3430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-dif 3436
This theorem is referenced by:  xpdifid  5276  boxcutc  7564  infeq5i  8132  cantnflem2  8185  ackbij1lem18  8656  infpssrlem4  8725  fin23lem30  8761  domtriomlem  8861  pwfseqlem4  9076  dprdfadd  17594  pgpfac1lem2  17649  pgpfac1lem3a  17650  pgpfac1lem3  17651  lspsolv  18307  lsppratlem3  18313  mplsubrglem  18604  frlmssuvc2  19290  hauscmplem  20358  1stccnp  20414  1stckgen  20506  alexsublem  20996  bcthlem4  22214  plyeq0lem  23071  ftalem3  23903  tglngne  24494  disjiunel  28086  ofpreima2  28150  qqhval2  28666  esum2dlem  28793  carsgclctunlem1  29019  sibfof  29042  sitgaddlemb  29050  eulerpartlemsv2  29058  eulerpartlemv  29064  eulerpartlemgs2  29080  dochnel2  34713  rmspecnonsq  35509  disjiun2  37087  dstregt0  37148  fprodexp  37294  fprodabs2  37295  lptre2pt  37340  dvnprodlem2  37439  stoweidlem43  37521  fourierdlem66  37652
  Copyright terms: Public domain W3C validator