Metamath Proof Explorer


Theorem indif

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

Ref Expression
Assertion indif A A B = A B

Proof

Step Hyp Ref Expression
1 dfin4 A A B = A A A B
2 dfin4 A B = A A B
3 2 difeq2i A A B = A A A B
4 difin A A B = A B
5 1 3 4 3eqtr2i A A B = A B