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