Definition df-nel 2510

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

This definition is referenced by:  neli  2511  nelir  2512  neleq1  2513  neleq2  2514  nfnel  2516  nfneld  2517  elnelne1  2518  elnelne2  2519  nelcon3d  2520  elnelall  2521  ru  3043  sbcnel12g  3157  raldifb  3361  pwnss  4274  pwnex  4572  ruALT  4675  0nelrel  4798  opabn1stprc  6391  fiprc  7059  0mnnnnn0  9530  nelfzo  10490  fvinim0ffz  10591  wrdlndm  11245  wrdsymb0  11261  rennim  11691  fsumsplitsnun  12109  modfsummodlemstep  12147  sqrt2irr0  12865  isnsgrp  13636  vtxvalprc  16067  iedgvalprc  16068  umgrnloop2  16163  1hevtxdg0fi  16319  p1evtxdeqfilem  16323  vdegp1aid  16326  eupth2lem3lem6fi  16483  bdnel  16641