This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ((A \times A) \cap (B \times B)) = A \cap B$

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