Theorem dfin4

Description: Alternate definition of the intersection of two classes. Exercise 4.10(q) of Mendelson p. 231. (Contributed by NM, 25-Nov-2003)

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

Proof

Step	Hyp	Ref	Expression
1		inss1	|- ( A i^i B ) C_ A
2		dfss4	|- ( ( A i^i B ) C_ A <-> ( A \ ( A \ ( A i^i B ) ) ) = ( A i^i B ) )
3	1 2	mpbi	|- ( A \ ( A \ ( A i^i B ) ) ) = ( A i^i B )
4		difin	|- ( A \ ( A i^i B ) ) = ( A \ B )
5	4	difeq2i	|- ( A \ ( A \ ( A i^i B ) ) ) = ( A \ ( A \ B ) )
6	3 5	eqtr3i	|- ( A i^i B ) = ( A \ ( A \ B ) )