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

Theorem nnel 3056
Description: Negation of negated membership, analogous to nne 2944. (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 3047 . . 3 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
21bicomi 224 . 2 𝐴𝐵𝐴𝐵)
32con1bii 356 1 𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wcel 2108  wnel 3046
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 207  df-nel 3047
This theorem is referenced by:  raldifsnb  4796  mpoxopynvov0g  8239  fsetexb  8904  0mnnnnn0  12558  ssnn0fi  14026  rabssnn0fi  14027  hashnfinnn0  14400  lcmfunsnlem2lem2  16676  finsumvtxdg2ssteplem1  29563  pthdivtx  29747  wwlksnndef  29925  frgrwopreglem4a  30329  poimirlem26  37653  sticksstones1  42147  afv2orxorb  47240  afv2fv0  47277  lswn0  47431  prminf2  47575  uspgrimprop  47873
  Copyright terms: Public domain W3C validator