Definition df-nel 2456

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

This definition is referenced by:  neli  2457  nelir  2458  neleq1  2459  neleq2  2460  nfnel  2462  nfneld  2463  elnelne1  2464  elnelne2  2465  nelcon3d  2466  elnelall  2467  ru  2976  sbcnel12g  3089  raldifb  3290  pwnss  4177  pwnex  4467  ruALT  4568  0nelrel  4690  fiprc  6841  0mnnnnn0  9238  fvinim0ffz  10271  rennim  11043  fsumsplitsnun  11459  modfsummodlemstep  11497  sqrt2irr0  12196  isnsgrp  12869  bdnel  15064