Definition df-nel 2443

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

This definition is referenced by:  neli  2444  nelir  2445  neleq1  2446  neleq2  2447  nfnel  2449  nfneld  2450  elnelne1  2451  elnelne2  2452  nelcon3d  2453  elnelall  2454  ru  2961  sbcnel12g  3074  raldifb  3275  pwnss  4159  pwnex  4449  ruALT  4550  0nelrel  4672  fiprc  6814  0mnnnnn0  9207  fvinim0ffz  10240  rennim  11010  fsumsplitsnun  11426  modfsummodlemstep  11464  sqrt2irr0  12163  isnsgrp  12811  bdnel  14576