Theorem dmxpin

Description: The domain of the intersection of two Cartesian squares. Unlike in dmin , equality holds. (Contributed by NM, 29-Jan-2008)

	Ref	Expression
Assertion	dmxpin	⊢ dom ( ( 𝐴 × 𝐴 ) ∩ ( 𝐵 × 𝐵 ) ) = ( 𝐴 ∩ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		inxp	⊢ ( ( 𝐴 × 𝐴 ) ∩ ( 𝐵 × 𝐵 ) ) = ( ( 𝐴 ∩ 𝐵 ) × ( 𝐴 ∩ 𝐵 ) )
2	1	dmeqi	⊢ dom ( ( 𝐴 × 𝐴 ) ∩ ( 𝐵 × 𝐵 ) ) = dom ( ( 𝐴 ∩ 𝐵 ) × ( 𝐴 ∩ 𝐵 ) )
3		dmxpid	⊢ dom ( ( 𝐴 ∩ 𝐵 ) × ( 𝐴 ∩ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 )
4	2 3	eqtri	⊢ dom ( ( 𝐴 × 𝐴 ) ∩ ( 𝐵 × 𝐵 ) ) = ( 𝐴 ∩ 𝐵 )