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  4296  pwnex  4595  ruALT  4698  0nelrel  4821  opabn1stprc  6429  fsetdmprc0  6950  fiprc  7104  0mnnnnn0  9599  nelfzo  10569  fvinim0ffz  10670  wrdlndm  11335  wrdsymb0  11351  rennim  11782  fsumsplitsnun  12202  modfsummodlemstep  12240  sqrt2irr0  12959  isnsgrp  13770  vtxvalprc  16394  iedgvalprc  16395  umgrnloop2  16490  1hevtxdg0fi  16646  p1evtxdeqfilem  16650  vdegp1aid  16653  eupth2lem3lem6fi  16810  bdnel  16978