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  4145  pwnex  4434  ruALT  4535  0nelrel  4657  fiprc  6793  0mnnnnn0  9167  fvinim0ffz  10197  rennim  10966  fsumsplitsnun  11382  modfsummodlemstep  11420  sqrt2irr0  12118  isnsgrp  12647  bdnel  13889