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

Metamath Proof Explorer

Theorem iunxpconst

Description: Membership in a union of Cartesian products when the second factor is constant. (Contributed by Mario Carneiro, 29-Dec-2014)

		Ref	Expression
	Assertion	iunxpconst	$⊢ ⋃_{x \in A} (\{x\} \times B) = A \times B$

Step	Hyp	Ref	Expression
1		xpiundir	$⊢ ⋃_{x \in A} \{x\} \times B = ⋃_{x \in A} (\{x\} \times B)$
2		iunid	$⊢ ⋃_{x \in A} \{x\} = A$
3	2	xpeq1i	$⊢ ⋃_{x \in A} \{x\} \times B = A \times B$
4	1 3	eqtr3i	$⊢ ⋃_{x \in A} (\{x\} \times B) = A \times B$