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

Theorem elndif 3473
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 3472 . 2  |-  ( A  e.  ( C  \  B )  ->  -.  A  e.  B )
21con2i 115 1  |-  ( A  e.  B  ->  -.  A  e.  ( C  \  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1726    \ cdif 3319
This theorem is referenced by:  peano5  4871  undifixp  7101  cantnfreslem  7634  ssfin4  8195  isf32lem3  8240  isf34lem4  8262  xrinfmss  10893  restntr  17251  cmpcld  17470  reconnlem2  18863  lebnumlem1  18991  i1fd  19576  dfon2lem6  25420  onsucconi  26192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-dif 3325
  Copyright terms: Public domain W3C validator