Theorem nnel

Description: Negation of negated membership, analogous to nne . (Contributed by Alexander van der Vekens, 18-Jan-2018) (Proof shortened by Wolf Lammen, 25-Nov-2019)

	Ref	Expression
Assertion	nnel	⊢ ( ¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵 )

Proof

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