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 referenced 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  4294  pwnex  4593  ruALT  4696  0nelrel  4819  opabn1stprc  6422  fsetdmprc0  6943  fiprc  7097  0mnnnnn0  9577  nelfzo  10540  fvinim0ffz  10641  wrdlndm  11302  wrdsymb0  11318  rennim  11749  fsumsplitsnun  12167  modfsummodlemstep  12205  sqrt2irr0  12923  isnsgrp  13701  vtxvalprc  16213  iedgvalprc  16214  umgrnloop2  16309  1hevtxdg0fi  16465  p1evtxdeqfilem  16469  vdegp1aid  16472  eupth2lem3lem6fi  16629  bdnel  16797