Definition df-nel 2496

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 2495	. 2 wff 𝐴 ∉ 𝐵
4	1, 2	wcel 2200	. . 3 wff 𝐴 ∈ 𝐵
5	4	wn 3	. 2 wff ¬ 𝐴 ∈ 𝐵
6	3, 5	wb 105	1 wff (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)

This definition is referenced by:  neli  2497  nelir  2498  neleq1  2499  neleq2  2500  nfnel  2502  nfneld  2503  elnelne1  2504  elnelne2  2505  nelcon3d  2506  elnelall  2507  ru  3027  sbcnel12g  3141  raldifb  3344  pwnss  4242  pwnex  4539  ruALT  4642  0nelrel  4764  fiprc  6966  0mnnnnn0  9397  nelfzo  10344  fvinim0ffz  10442  wrdlndm  11083  wrdsymb0  11099  rennim  11508  fsumsplitsnun  11925  modfsummodlemstep  11963  sqrt2irr0  12681  isnsgrp  13434  vtxvalprc  15850  iedgvalprc  15851  umgrnloop2  15943  bdnel  16175