This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( ¬ 𝐴 ∉ 𝐵 ↔ 𝐴 ∈ 𝐵 )