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  4243  pwnex  4540  ruALT  4643  0nelrel  4765  fiprc  6976  0mnnnnn0  9412  nelfzo  10360  fvinim0ffz  10459  wrdlndm  11101  wrdsymb0  11117  rennim  11528  fsumsplitsnun  11945  modfsummodlemstep  11983  sqrt2irr0  12701  isnsgrp  13454  vtxvalprc  15871  iedgvalprc  15872  umgrnloop2  15964  bdnel  16272