Definition df-nel 2472

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 2471	. 2 wff A e/ B
4	1, 2	wcel 2176	. . 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  2473  nelir  2474  neleq1  2475  neleq2  2476  nfnel  2478  nfneld  2479  elnelne1  2480  elnelne2  2481  nelcon3d  2482  elnelall  2483  ru  2997  sbcnel12g  3110  raldifb  3313  pwnss  4204  pwnex  4497  ruALT  4600  0nelrel  4722  fiprc  6909  0mnnnnn0  9329  nelfzo  10276  fvinim0ffz  10372  wrdlndm  11013  wrdsymb0  11028  rennim  11346  fsumsplitsnun  11763  modfsummodlemstep  11801  sqrt2irr0  12519  isnsgrp  13271  vtxvalprc  15683  iedgvalprc  15684  bdnel  15827