Theorem indif

Description: Intersection with class difference. Theorem 34 of Suppes p. 29. (Contributed by NM, 17-Aug-2004)

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

Proof

Step	Hyp	Ref	Expression
1		dfin4	|- ( A i^i ( A \ B ) ) = ( A \ ( A \ ( A \ B ) ) )
2		dfin4	|- ( A i^i B ) = ( A \ ( A \ B ) )
3	2	difeq2i	|- ( A \ ( A i^i B ) ) = ( A \ ( A \ ( A \ B ) ) )
4		difin	|- ( A \ ( A i^i B ) ) = ( A \ B )
5	1 3 4	3eqtr2i	|- ( A i^i ( A \ B ) ) = ( A \ B )