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

Theorem nnel 3132
Description: Negation of negated membership, analogous to nne 3020. (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 3124 . . 3 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
21bicomi 226 . 2 𝐴𝐵𝐴𝐵)
32con1bii 359 1 𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 208  wcel 2110  wnel 3123
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 209  df-nel 3124
This theorem is referenced by:  raldifsnb  4728  mpoxopynvov0g  7879  0mnnnnn0  11928  ssnn0fi  13352  rabssnn0fi  13353  hashnfinnn0  13721  lcmfunsnlem2lem2  15982  finsumvtxdg2ssteplem1  27326  pthdivtx  27509  wwlksnndef  27682  wwlksnfiOLD  27684  frgrwopreglem4a  28088  poimirlem26  34917  afv2orxorb  43428  afv2fv0  43465  lswn0  43605  prminf2  43751
  Copyright terms: Public domain W3C validator