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 used 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  4298  pwnex  4597  ruALT  4700  0nelrel  4823  opabn1stprc  6433  fsetdmprc0  6954  fiprc  7108  0mnnnnn0  9606  nelfzo  10576  fvinim0ffz  10677  wrdlndm  11343  wrdsymb0  11359  rennim  11790  fsumsplitsnun  12211  modfsummodlemstep  12249  sqrt2irr0  12968  isnsgrp  13780  vtxvalprc  16501  iedgvalprc  16502  umgrnloop2  16597  1hevtxdg0fi  16753  p1evtxdeqfilem  16757  vdegp1aid  16760  eupth2lem3lem6fi  16917  bdnel  17085