Theorem nnel 2906

Description: Negation of negated membership, analogous to nne 2798. (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 2898	. . 3 ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)
2	1	bicomi 214	. 2 ⊢ (¬ 𝐴 ∈ 𝐵 ↔ 𝐴 ∉ 𝐵)
3	2	con1bii 346	1 ⊢ (¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵)

Syntax hints:  ¬ wn 3   ↔ wb 196   ∈ wcel 1990   ∉ wnel 2897

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 197  df-nel 2898

This theorem is referenced by:  raldifsnb  4325  mpt2xopynvov0g  7340  0mnnnnn0  11325  ssnn0fi  12784  rabssnn0fi  12785  hashnfinnn0  13152  lcmfunsnlem2lem2  15352  finsumvtxdg2ssteplem1  26441  pthdivtx  26625  wwlksnndef  26800  wwlksnfi  26801  clwwlksnndef  26890  frgrwopreglem4a  27174  poimirlem26  33435  lswn0  41380  prminf2  41500