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  4203  pwnex  4496  ruALT  4599  0nelrel  4721  fiprc  6907  0mnnnnn0  9327  nelfzo  10274  fvinim0ffz  10370  wrdlndm  11011  wrdsymb0  11026  rennim  11313  fsumsplitsnun  11730  modfsummodlemstep  11768  sqrt2irr0  12486  isnsgrp  13238  vtxvalprc  15650  iedgvalprc  15651  bdnel  15794