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

Theorem nnel 3047
Description: Negation of negated membership, analogous to nne 2938. (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 3039 . . 3 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
21bicomi 227 . 2 𝐴𝐵𝐴𝐵)
32con1bii 360 1 𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wcel 2113  wnel 3038
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 210  df-nel 3039
This theorem is referenced by:  raldifsnb  4685  mpoxopynvov0g  7910  fsetexb  8475  0mnnnnn0  12009  ssnn0fi  13445  rabssnn0fi  13446  hashnfinnn0  13815  lcmfunsnlem2lem2  16081  finsumvtxdg2ssteplem1  27487  pthdivtx  27670  wwlksnndef  27843  frgrwopreglem4a  28247  poimirlem26  35423  sticksstones1  39705  afv2orxorb  44245  afv2fv0  44282  lswn0  44422  prminf2  44566
  Copyright terms: Public domain W3C validator