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	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = ( 𝐴 × 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		xpiundir	⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑥 } × 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
2		iunid	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴
3	2	xpeq1i	⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑥 } × 𝐵 ) = ( 𝐴 × 𝐵 )
4	1 3	eqtr3i	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = ( 𝐴 × 𝐵 )