Definition df-nel 2431

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

This definition is referenced by:  neli  2432  nelir  2433  neleq1  2434  neleq2  2435  nfnel  2437  nfneld  2438  elnelne1  2439  elnelne2  2440  nelcon3d  2441  elnelall  2442  ru  2949  sbcnel12g  3061  raldifb  3261  pwnss  4137  pwnex  4426  ruALT  4527  0nelrel  4649  fiprc  6777  0mnnnnn0  9142  fvinim0ffz  10172  rennim  10940  fsumsplitsnun  11356  modfsummodlemstep  11394  sqrt2irr0  12092  bdnel  13696