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

Step	Hyp	Ref	Expression
1		df-nel 2783	. . 3 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
2	1	bicomi 213	. 2 ⊢ (¬ 𝐴 ∈ 𝐵 ↔ 𝐴 ∉ 𝐵)
3	2	con1bii 345	1 ⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵)

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