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

Theorem nnel 3083
Description: Negation of negated membership, analogous to nne 2975. (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 3075 . . 3 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
21bicomi 216 . 2 𝐴𝐵𝐴𝐵)
32con1bii 348 1 𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 198  wcel 2157  wnel 3074
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 199  df-nel 3075
This theorem is referenced by:  raldifsnb  4515  mpt2xopynvov0g  7578  0mnnnnn0  11614  ssnn0fi  13039  rabssnn0fi  13040  hashnfinnn0  13402  lcmfunsnlem2lem2  15687  finsumvtxdg2ssteplem1  26795  pthdivtx  26983  wwlksnndef  27185  wwlksnfi  27186  frgrwopreglem4a  27659  poimirlem26  33924  afv2orxorb  42082  afv2fv0  42119  lswn0  42220  prminf2  42282
  Copyright terms: Public domain W3C validator