Definition df-nel 2207

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

Assertion

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

Detailed syntax breakdown of Definition df-nel

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	wnel 2205	. 2 wff 𝐴 ∉ 𝐵
4	1, 2	wcel 1393	. . 3 wff 𝐴 ∈ 𝐵
5	4	wn 3	. 2 wff ¬ 𝐴 ∈ 𝐵
6	3, 5	wb 98	1 wff (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)

This definition is referenced by:  neli  2299  nelir  2300  neleq1  2301  neleq2  2302  nfnel  2304  nfneld  2305  ru  2763  sbcnel12g  2867  raldifb  3083  pwnss  3912  ruALT  4275  fiprc  6292  0mnnnnn0  8214  fvinim0ffz  9096  rennim  9600  bdnel  9974