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  3044  sbcnel12g  3158  raldifb  3363  pwnss  4277  pwnex  4575  ruALT  4678  0nelrel  4801  opabn1stprc  6402  fiprc  7070  0mnnnnn0  9545  nelfzo  10508  fvinim0ffz  10609  wrdlndm  11266  wrdsymb0  11282  rennim  11712  fsumsplitsnun  12130  modfsummodlemstep  12168  sqrt2irr0  12886  isnsgrp  13669  vtxvalprc  16176  iedgvalprc  16177  umgrnloop2  16272  1hevtxdg0fi  16428  p1evtxdeqfilem  16432  vdegp1aid  16435  eupth2lem3lem6fi  16592  bdnel  16750