Description: Bring an intersection in and out of a class difference. (Contributed by Mario Carneiro, 15-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | indif1 | ⊢ ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | indif2 | ⊢ ( 𝐵 ∩ ( 𝐴 ∖ 𝐶 ) ) = ( ( 𝐵 ∩ 𝐴 ) ∖ 𝐶 ) | |
2 | incom | ⊢ ( 𝐵 ∩ ( 𝐴 ∖ 𝐶 ) ) = ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) | |
3 | incom | ⊢ ( 𝐵 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 ) | |
4 | 3 | difeq1i | ⊢ ( ( 𝐵 ∩ 𝐴 ) ∖ 𝐶 ) = ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) |
5 | 1 2 4 | 3eqtr3i | ⊢ ( ( 𝐴 ∖ 𝐶 ) ∩ 𝐵 ) = ( ( 𝐴 ∩ 𝐵 ) ∖ 𝐶 ) |