Definition df-nel 2340

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 2339	. 2 wff 𝐴 ∉ 𝐵
4	1, 2	wcel 1433	. . 3 wff 𝐴 ∈ 𝐵
5	4	wn 3	. 2 wff ¬ 𝐴 ∈ 𝐵
6	3, 5	wb 103	1 wff (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)

This definition is referenced by:  neli  2341  nelir  2342  neleq1  2343  neleq2  2344  nfnel  2346  nfneld  2347  ru  2814  sbcnel12g  2923  raldifb  3112  pwnss  3933  ruALT  4294  fiprc  6315  0mnnnnn0  8320  fvinim0ffz  9250  rennim  9888  bdnel  10645