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

Theorem nnel 2935
Description: Negation of negated membership, analogous to nne 2827. (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 2927 . . 3 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
21bicomi 214 . 2 𝐴𝐵𝐴𝐵)
32con1bii 345 1 𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wcel 2030  wnel 2926
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 197  df-nel 2927
This theorem is referenced by:  raldifsnb  4358  mpt2xopynvov0g  7385  0mnnnnn0  11363  ssnn0fi  12824  rabssnn0fi  12825  hashnfinnn0  13190  lcmfunsnlem2lem2  15399  finsumvtxdg2ssteplem1  26497  pthdivtx  26681  wwlksnndef  26868  wwlksnfi  26869  frgrwopreglem4a  27290  poimirlem26  33565  lswn0  41705  prminf2  41825
  Copyright terms: Public domain W3C validator