Definition df-nel

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

	Ref	Expression
Assertion	df-nel	⊢ ( 𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	wnel	⊢ 𝐴 ∉ 𝐵
3	0 1	wcel	⊢ 𝐴 ∈ 𝐵
4	3	wn	⊢ ¬ 𝐴 ∈ 𝐵
5	2 4	wb	⊢ ( 𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵 )