Theorem difdif

Description: Double class difference. Exercise 11 of TakeutiZaring p. 22. (Contributed by NM, 17-May-1998)

	Ref	Expression
Assertion	difdif	|- ( A \ ( B \ A ) ) = A

Proof

Step	Hyp	Ref	Expression
1		pm4.45im	|- ( x e. A <-> ( x e. A /\ ( x e. B -> x e. A ) ) )
2		iman	|- ( ( x e. B -> x e. A ) <-> -. ( x e. B /\ -. x e. A ) )
3		eldif	|- ( x e. ( B \ A ) <-> ( x e. B /\ -. x e. A ) )
4	2 3	xchbinxr	|- ( ( x e. B -> x e. A ) <-> -. x e. ( B \ A ) )
5	4	anbi2i	|- ( ( x e. A /\ ( x e. B -> x e. A ) ) <-> ( x e. A /\ -. x e. ( B \ A ) ) )
6	1 5	bitr2i	|- ( ( x e. A /\ -. x e. ( B \ A ) ) <-> x e. A )
7	6	difeqri	|- ( A \ ( B \ A ) ) = A