Metamath Proof Explorer


Theorem inin

Description: Intersection with an intersection. (Contributed by Thierry Arnoux, 27-Dec-2016)

Ref Expression
Assertion inin ( 𝐴 ∩ ( 𝐴𝐵 ) ) = ( 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 in13 ( 𝐴 ∩ ( 𝐴𝐵 ) ) = ( 𝐵 ∩ ( 𝐴𝐴 ) )
2 inidm ( 𝐴𝐴 ) = 𝐴
3 2 ineq2i ( 𝐵 ∩ ( 𝐴𝐴 ) ) = ( 𝐵𝐴 )
4 incom ( 𝐵𝐴 ) = ( 𝐴𝐵 )
5 1 3 4 3eqtri ( 𝐴 ∩ ( 𝐴𝐵 ) ) = ( 𝐴𝐵 )