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

Theorem nnel 3044
Description: Negation of negated membership, analogous to nne 2936. (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 3036 . . 3 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
21bicomi 214 . 2 𝐴𝐵𝐴𝐵)
32con1bii 345 1 𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wcel 2139  wnel 3035
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 3036
This theorem is referenced by:  raldifsnb  4471  mpt2xopynvov0g  7509  0mnnnnn0  11517  ssnn0fi  12978  rabssnn0fi  12979  hashnfinnn0  13344  lcmfunsnlem2lem2  15554  finsumvtxdg2ssteplem1  26651  pthdivtx  26835  wwlksnndef  27023  wwlksnfi  27024  frgrwopreglem4a  27464  poimirlem26  33748  lswn0  41890  prminf2  42010
  Copyright terms: Public domain W3C validator