Theorem difin

Description: Difference with intersection. Theorem 33 of Suppes p. 29. (Contributed by NM, 31-Mar-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011)

	Ref	Expression
Assertion	difin	|- ( A \ ( A i^i B ) ) = ( A \ B )

Proof

Step	Hyp	Ref	Expression
1		pm4.61	|- ( -. ( x e. A -> x e. B ) <-> ( x e. A /\ -. x e. B ) )
2		anclb	|- ( ( x e. A -> x e. B ) <-> ( x e. A -> ( x e. A /\ x e. B ) ) )
3		elin	|- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
4	3	imbi2i	|- ( ( x e. A -> x e. ( A i^i B ) ) <-> ( x e. A -> ( x e. A /\ x e. B ) ) )
5		iman	|- ( ( x e. A -> x e. ( A i^i B ) ) <-> -. ( x e. A /\ -. x e. ( A i^i B ) ) )
6	2 4 5	3bitr2i	|- ( ( x e. A -> x e. B ) <-> -. ( x e. A /\ -. x e. ( A i^i B ) ) )
7	6	con2bii	|- ( ( x e. A /\ -. x e. ( A i^i B ) ) <-> -. ( x e. A -> x e. B ) )
8		eldif	|- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
9	1 7 8	3bitr4i	|- ( ( x e. A /\ -. x e. ( A i^i B ) ) <-> x e. ( A \ B ) )
10	9	difeqri	|- ( A \ ( A i^i B ) ) = ( A \ B )