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	$$⊢\mathrm{dom}\left(\left(A\times A\right)\cap \left(B\times B\right)\right)=A\cap B$$

Proof

Step	Hyp	Ref	Expression
1		inxp	$$⊢\left(A\times A\right)\cap \left(B\times B\right)=\left(A\cap B\right)\times \left(A\cap B\right)$$
2	1	dmeqi	$$⊢\mathrm{dom}\left(\left(A\times A\right)\cap \left(B\times B\right)\right)=\mathrm{dom}\left(\left(A\cap B\right)\times \left(A\cap B\right)\right)$$
3		dmxpid	$$⊢\mathrm{dom}\left(\left(A\cap B\right)\times \left(A\cap B\right)\right)=A\cap B$$
4	2 3	eqtri	$$⊢\mathrm{dom}\left(\left(A\times A\right)\cap \left(B\times B\right)\right)=A\cap B$$