Definition df-nel 2436

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

This definition is referenced by:  neli  2437  nelir  2438  neleq1  2439  neleq2  2440  nfnel  2442  nfneld  2443  elnelne1  2444  elnelne2  2445  nelcon3d  2446  elnelall  2447  ru  2954  sbcnel12g  3066  raldifb  3267  pwnss  4143  pwnex  4432  ruALT  4533  0nelrel  4655  fiprc  6789  0mnnnnn0  9154  fvinim0ffz  10184  rennim  10953  fsumsplitsnun  11369  modfsummodlemstep  11407  sqrt2irr0  12105  isnsgrp  12634  bdnel  13849