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  2962  sbcnel12g  3075  raldifb  3276  pwnss  4160  pwnex  4450  ruALT  4551  0nelrel  4673  fiprc  6815  0mnnnnn0  9208  fvinim0ffz  10241  rennim  11011  fsumsplitsnun  11427  modfsummodlemstep  11465  sqrt2irr0  12164  isnsgrp  12812  bdnel  14609