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	$$⊢\neg A\notin B\leftrightarrow A\in B$$

Proof

Step	Hyp	Ref	Expression
1		df-nel	$$⊢A\notin B\leftrightarrow \neg A\in B$$
2	1	bicomi	$$⊢\neg A\in B\leftrightarrow A\notin B$$
3	2	con1bii	$$⊢\neg A\notin B\leftrightarrow A\in B$$