Definition df-nel 2498

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 2497	. 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  2499  nelir  2500  neleq1  2501  neleq2  2502  nfnel  2504  nfneld  2505  elnelne1  2506  elnelne2  2507  nelcon3d  2508  elnelall  2509  ru  3030  sbcnel12g  3144  raldifb  3347  pwnss  4249  pwnex  4546  ruALT  4649  0nelrel  4772  opabn1stprc  6358  fiprc  6990  0mnnnnn0  9434  nelfzo  10387  fvinim0ffz  10488  wrdlndm  11134  wrdsymb0  11150  rennim  11580  fsumsplitsnun  11998  modfsummodlemstep  12036  sqrt2irr0  12754  isnsgrp  13507  vtxvalprc  15925  iedgvalprc  15926  umgrnloop2  16021  1hevtxdg0fi  16177  p1evtxdeqfilem  16181  vdegp1aid  16184  eupth2lem3lem6fi  16341  bdnel  16500