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

Theorem nnel 2802
Description: Negation of negated membership, analogous to nne 2658. (Contributed by Alexander van der Vekens, 18-Jan-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
Assertion
Ref Expression
nnel

Proof of Theorem nnel
StepHypRef Expression
1 df-nel 2655 . . 3
21bicomi 202 . 2
32con1bii 331 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  e.wcel 1818  e/wnel 2653
This theorem is referenced by:  raldifsnb  4161  mpt2xopynvov0g  6961  0mnnnnn0  10853  ssnn0fi  12094  rabssnn0fi  12095  hashnfinnn0  12432  nbgranself2  24436  cusgrasizeindslem2  24474  wwlknndef  24737  wwlknfi  24738  clwwlknndef  24773  frgrawopreglem4  25047  lswn0  32343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-nel 2655
  Copyright terms: Public domain W3C validator