Definition df-nel 2496

Description: Define negated membership. (Contributed by NM, 7-Aug-1994.)

Assertion

Ref	Expression
df-nel	|- ( A e/ B <-> -. A e. B )

Detailed syntax breakdown of Definition df-nel

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wnel 2495	. 2 wff A e/ B
4	1, 2	wcel 2200	. . 3 wff A e. B
5	4	wn 3	. 2 wff -. A e. B
6	3, 5	wb 105	1 wff ( A e/ B <-> -. A e. B )

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  6968  0mnnnnn0  9401  nelfzo  10348  fvinim0ffz  10447  wrdlndm  11088  wrdsymb0  11104  rennim  11513  fsumsplitsnun  11930  modfsummodlemstep  11968  sqrt2irr0  12686  isnsgrp  13439  vtxvalprc  15856  iedgvalprc  15857  umgrnloop2  15949  bdnel  16217