Definition df-nel

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

	Ref	Expression
Assertion	df-nel	|- ( A e/ B <-> -. A e. B )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	wnel	|- A e/ B
3	0 1	wcel	|- A e. B
4	3	wn	|- -. A e. B
5	2 4	wb	|- ( A e/ B <-> -. A e. B )