Definition df-nel 2455

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

This definition is referenced by:  neli  2456  nelir  2457  neleq1  2458  neleq2  2459  nfnel  2461  nfneld  2462  elnelne1  2463  elnelne2  2464  nelcon3d  2465  elnelall  2466  ru  2975  sbcnel12g  3088  raldifb  3289  pwnss  4173  pwnex  4463  ruALT  4564  0nelrel  4686  fiprc  6832  0mnnnnn0  9225  fvinim0ffz  10258  rennim  11028  fsumsplitsnun  11444  modfsummodlemstep  11482  sqrt2irr0  12181  isnsgrp  12834  bdnel  14989