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	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)=A\times B$$

Proof

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