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  6357  fiprc  6989  0mnnnnn0  9433  nelfzo  10386  fvinim0ffz  10486  wrdlndm  11129  wrdsymb0  11145  rennim  11562  fsumsplitsnun  11979  modfsummodlemstep  12017  sqrt2irr0  12735  isnsgrp  13488  vtxvalprc  15905  iedgvalprc  15906  umgrnloop2  16001  1hevtxdg0fi  16157  p1evtxdeqfilem  16161  vdegp1aid  16164  bdnel  16449