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  3028  sbcnel12g  3142  raldifb  3345  pwnss  4247  pwnex  4544  ruALT  4647  0nelrel  4770  opabn1stprc  6353  fiprc  6985  0mnnnnn0  9424  nelfzo  10377  fvinim0ffz  10477  wrdlndm  11120  wrdsymb0  11136  rennim  11553  fsumsplitsnun  11970  modfsummodlemstep  12008  sqrt2irr0  12726  isnsgrp  13479  vtxvalprc  15896  iedgvalprc  15897  umgrnloop2  15990  1hevtxdg0fi  16113  bdnel  16385