Definition df-nel 2315

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

This definition is referenced by:  neli  2316  nelir  2317  neleq1  2318  neleq2  2319  nfnel  2321  nfneld  2322  ru  2785  sbcnel12g  2894  raldifb  3110  pwnss  3939  ruALT  4302  fiprc  6322  0mnnnnn0  8270  fvinim0ffz  9197  rennim  9828  bdnel  10340