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

Theorem elndif 3546
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 3545 . 2  |-  ( A  e.  ( C  \  B )  ->  -.  A  e.  B )
21con2i 124 1  |-  ( A  e.  B  ->  -.  A  e.  ( C  \  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1904    \ cdif 3387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-dif 3393
This theorem is referenced by:  peano5  6735  extmptsuppeq  6958  undifixp  7576  ssfin4  8758  isf32lem3  8803  isf34lem4  8825  xrinfmss  11620  restntr  20275  cmpcld  20494  reconnlem2  21923  lebnumlem1  22067  lebnumlem1OLD  22070  i1fd  22718  dfon2lem6  30505  onsucconi  31168  caragendifcl  38454
  Copyright terms: Public domain W3C validator