Definition df-nel 2499

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

This definition is referenced by:  neli  2500  nelir  2501  neleq1  2502  neleq2  2503  nfnel  2505  nfneld  2506  elnelne1  2507  elnelne2  2508  nelcon3d  2509  elnelall  2510  ru  3031  sbcnel12g  3145  raldifb  3349  pwnss  4255  pwnex  4552  ruALT  4655  0nelrel  4778  opabn1stprc  6367  fiprc  7033  0mnnnnn0  9493  nelfzo  10449  fvinim0ffz  10550  wrdlndm  11196  wrdsymb0  11212  rennim  11642  fsumsplitsnun  12060  modfsummodlemstep  12098  sqrt2irr0  12816  isnsgrp  13569  vtxvalprc  15996  iedgvalprc  15997  umgrnloop2  16092  1hevtxdg0fi  16248  p1evtxdeqfilem  16252  vdegp1aid  16255  eupth2lem3lem6fi  16412  bdnel  16570