Definition df-dif

Description: Define class difference, also called relative complement. Definition 5.12 of TakeutiZaring p. 20. For example, ( { 1 , 3 } \ { 1 , 8 } ) = { 3 } ( ex-dif ). Contrast this operation with union ( A u. B ) ( df-un ) and intersection ( A i^i B ) ( df-in ). Several notations are used in the literature; we chose the \ convention used in Definition 5.3 of Eisenberg p. 67 instead of the more common minus sign to reserve the latter for later use in, e.g., arithmetic. We will use the terminology " A excludes B " to mean A \ B . We will use " B is removed from A " to mean A \ { B } i.e. the removal of an element or equivalently the exclusion of a singleton. (Contributed by NM, 29-Apr-1994)

	Ref	Expression
Assertion	df-dif	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	cdif	|- ( A \ B )
3		vx	|- x
4	3	cv	|- x
5	4 0	wcel	|- x e. A
6	4 1	wcel	|- x e. B
7	6	wn	|- -. x e. B
8	5 7	wa	|- ( x e. A /\ -. x e. B )
9	8 3	cab	|- { x | ( x e. A /\ -. x e. B ) }
10	2 9	wceq	|- ( A \ B ) = { x | ( x e. A /\ -. x e. B ) }