Definition df-nel 2516

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 2515	. 2 wff A e/ B
4	1, 2	wcel 2209	. . 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 used by:  neli  2517  nelir  2518  neleq1  2519  neleq2  2520  nfnel  2522  nfneld  2523  elnelne1  2524  elnelne2  2525  nelcon3d  2526  elnelall  2527  ru  3050  sbcnel12g  3164  raldifb  3369  pwnss  4298  pwnex  4597  ruALT  4700  0nelrel  4823  opabn1stprc  6433  fsetdmprc0  6955  fiprc  7110  0mnnnnn0  9606  nelfzo  10575  fvinim0ffz  10676  wrdlndm  11342  wrdsymb0  11358  rennim  11789  fsumsplitsnun  12210  modfsummodlemstep  12248  sqrt2irr0  12967  isnsgrp  13779  vtxvalprc  16518  iedgvalprc  16519  umgrnloop2  16614  1hevtxdg0fi  16770  p1evtxdeqfilem  16774  vdegp1aid  16777  eupth2lem3lem6fi  16934  bdnel  17102