Definition df-nel 2347

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 2346	. 2 wff A e/ B
4	1, 2	wcel 1436	. . 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  2348  nelir  2349  neleq1  2350  neleq2  2351  nfnel  2353  nfneld  2354  ru  2828  sbcnel12g  2937  raldifb  3129  pwnss  3971  ruALT  4342  fiprc  6486  0mnnnnn0  8641  fvinim0ffz  9583  rennim  10334  fsumsplitsnun  10700  bdnel  11214