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

Theorem nnel 2892
Description: Negation of negated membership, analogous to nne 2786. (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 2783 . . 3 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
21bicomi 213 . 2 𝐴𝐵𝐴𝐵)
32con1bii 345 1 𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 195  wcel 1977  wnel 2781
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 196  df-nel 2783
This theorem is referenced by:  raldifsnb  4266  mpt2xopynvov0g  7205  0mnnnnn0  11175  ssnn0fi  12604  rabssnn0fi  12605  hashnfinnn0  12968  lcmfunsnlem2lem2  15139  nbgranself2  25759  cusgrasizeindslem1  25796  wwlknndef  26059  wwlknfi  26060  clwwlknndef  26095  frgrawopreglem4  26368  poimirlem26  32399  prminf2  39833  lswn0  40037  pthdivtx  40927  wwlksnndef  41103  wwlksnfi  41104  clwwlksnndef  41190  frgrwopreglem4  41476
  Copyright terms: Public domain W3C validator