Definition df-nel 2345

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

This definition is referenced by:  neli  2346  nelir  2347  neleq1  2348  neleq2  2349  nfnel  2351  nfneld  2352  ru  2824  sbcnel12g  2933  raldifb  3123  pwnss  3954  ruALT  4323  fiprc  6383  0mnnnnn0  8464  fvinim0ffz  9404  rennim  10114  bdnel  10937