Definition df-nel

Description: Define negated membership. (Contributed by NM, 7-Aug-1994)

	Ref	Expression
Assertion	df-nel	$$⊢A\notin B\leftrightarrow \neg A\in B$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	wnel	$$wffA\notin B$$
3	0 1	wcel	$$wffA\in B$$
4	3	wn	$$wff\neg A\in B$$
5	2 4	wb	$$wff\left(A\notin B\leftrightarrow \neg A\in B\right)$$