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

Theorem nnel 3059
Description: Negation of negated membership, analogous to nne 2948. (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 3051 . . 3 (𝐴𝐵 ↔ ¬ 𝐴𝐵)
21bicomi 223 . 2 𝐴𝐵𝐴𝐵)
32con1bii 357 1 𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wcel 2107  wnel 3050
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 3051
This theorem is referenced by:  raldifsnb  4761  mpoxopynvov0g  8150  fsetexb  8809  0mnnnnn0  12452  ssnn0fi  13897  rabssnn0fi  13898  hashnfinnn0  14268  lcmfunsnlem2lem2  16522  finsumvtxdg2ssteplem1  28535  pthdivtx  28719  wwlksnndef  28892  frgrwopreglem4a  29296  poimirlem26  36133  sticksstones1  40583  afv2orxorb  45534  afv2fv0  45571  lswn0  45710  prminf2  45854
  Copyright terms: Public domain W3C validator