Definition df-nel 2405

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 2404	. 2 wff A e/ B
4	1, 2	wcel 1481	. . 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  2406  nelir  2407  neleq1  2408  neleq2  2409  nfnel  2411  nfneld  2412  elnelne1  2413  elnelne2  2414  nelcon3d  2415  elnelall  2416  ru  2912  sbcnel12g  3024  raldifb  3221  pwnss  4091  pwnex  4378  ruALT  4474  0nelrel  4593  fiprc  6717  0mnnnnn0  9033  fvinim0ffz  10049  rennim  10806  fsumsplitsnun  11220  modfsummodlemstep  11258  sqrt2irr0  11878  bdnel  13223