Definition df-nel 2516

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

This definition is referenced by:  neli  2517  nelir  2518  neleq1  2519  neleq2  2520  nfnel  2522  nfneld  2523  elnelne1  2524  elnelne2  2525  nelcon3d  2526  elnelall  2527  ru  3050  sbcnel12g  3164  raldifb  3369  pwnss  4291  pwnex  4590  ruALT  4693  0nelrel  4816  opabn1stprc  6419  fsetdmprc0  6940  fiprc  7094  0mnnnnn0  9574  nelfzo  10537  fvinim0ffz  10638  wrdlndm  11299  wrdsymb0  11315  rennim  11746  fsumsplitsnun  12164  modfsummodlemstep  12202  sqrt2irr0  12920  isnsgrp  13698  vtxvalprc  16210  iedgvalprc  16211  umgrnloop2  16306  1hevtxdg0fi  16462  p1evtxdeqfilem  16466  vdegp1aid  16469  eupth2lem3lem6fi  16626  bdnel  16794