Definition df-nel 2404

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 2403	. 2 wff A e/ B
4	1, 2	wcel 1480	. . 3 wff A e. B
5	4	wn 3	. 2 wff -. A e. B
6	3, 5	wb 104	1 wff ( A e/ B <-> -. A e. B )

This definition is referenced by:  neli  2405  nelir  2406  neleq1  2407  neleq2  2408  nfnel  2410  nfneld  2411  elnelne1  2412  elnelne2  2413  nelcon3d  2414  elnelall  2415  ru  2908  sbcnel12g  3019  raldifb  3216  pwnss  4083  pwnex  4370  ruALT  4466  0nelrel  4585  fiprc  6709  0mnnnnn0  9009  fvinim0ffz  10018  rennim  10774  fsumsplitsnun  11188  modfsummodlemstep  11226  sqrt2irr0  11842  bdnel  13052