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

Theorem elndif 3387
Description: A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.)
Assertion
Ref Expression
elndif  |-  ( A  e.  B  ->  -.  A  e.  ( C  \  B ) )

Proof of Theorem elndif
StepHypRef Expression
1 eldifn 3386 . 2  |-  ( A  e.  ( C  \  B )  ->  -.  A  e.  B )
21con2i 112 1  |-  ( A  e.  B  ->  -.  A  e.  ( C  \  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1715    \ cdif 3235
This theorem is referenced by:  peano5  4782  fsnunf2  5832  undifixp  6995  cantnfreslem  7524  dfac9  7909  ssfin4  8083  isf32lem3  8128  isf34lem4  8150  xrinfmss  10781  restntr  17129  cmpcld  17346  reconnlem2  18546  lebnumlem1  18674  i1fd  19251  dfon2lem6  24970  onsucconi  25703  uvcff  26831  islindf4  26899
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-dif 3241
  Copyright terms: Public domain W3C validator