Definition df-nel 2363

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

This definition is referenced by:  neli  2364  nelir  2365  neleq1  2366  neleq2  2367  nfnel  2369  nfneld  2370  elnelne1  2371  elnelne2  2372  nelcon3d  2373  elnelall  2374  ru  2861  sbcnel12g  2970  raldifb  3163  pwnss  4023  pwnex  4308  ruALT  4404  0nelrel  4523  fiprc  6639  0mnnnnn0  8861  fvinim0ffz  9859  rennim  10614  fsumsplitsnun  11027  modfsummodlemstep  11065  bdnel  12633