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

Theorem nnel 3058
Description: Negation of negated membership, analogous to nne 2947. (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 3050 . . 3 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
21bicomi 223 . 2 𝐴𝐵𝐴𝐵)
32con1bii 357 1 𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wcel 2106  wnel 3049
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 206  df-nel 3050
This theorem is referenced by:  raldifsnb  4729  mpoxopynvov0g  8030  fsetexb  8652  0mnnnnn0  12265  ssnn0fi  13705  rabssnn0fi  13706  hashnfinnn0  14076  lcmfunsnlem2lem2  16344  finsumvtxdg2ssteplem1  27912  pthdivtx  28097  wwlksnndef  28270  frgrwopreglem4a  28674  poimirlem26  35803  sticksstones1  40102  afv2orxorb  44720  afv2fv0  44757  lswn0  44896  prminf2  45040
  Copyright terms: Public domain W3C validator