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 AAB=AB

Proof

Step Hyp Ref Expression
1 dfin4 AAB=AAAB
2 dfin4 AB=AAB
3 2 difeq2i AAB=AAAB
4 difin AAB=AB
5 1 3 4 3eqtr2i AAB=AB