Description: Intersection with an intersection. (Contributed by Thierry Arnoux, 27-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | inin | ⊢ ( 𝐴 ∩ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | in13 | ⊢ ( 𝐴 ∩ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐵 ∩ ( 𝐴 ∩ 𝐴 ) ) | |
2 | inidm | ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴 | |
3 | 2 | ineq2i | ⊢ ( 𝐵 ∩ ( 𝐴 ∩ 𝐴 ) ) = ( 𝐵 ∩ 𝐴 ) |
4 | incom | ⊢ ( 𝐵 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 ) | |
5 | 1 3 4 | 3eqtri | ⊢ ( 𝐴 ∩ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 ) |