Theorem xpiun

Description: A Cartesian product expressed as indexed union of ordered-pair class abstractions. (Contributed by AV, 27-Jan-2020)

	Ref	Expression
Assertion	xpiun	⊢ ( 𝐵 × 𝐶 ) = ∪ 𝑥 ∈ 𝐵 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 = 𝑥 ∧ 𝑏 ∈ 𝐶 ) }

Proof

Step	Hyp	Ref	Expression
1		xpsnopab	⊢ ( { 𝑥 } × 𝐶 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 = 𝑥 ∧ 𝑏 ∈ 𝐶 ) }
2	1	eqcomi	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 = 𝑥 ∧ 𝑏 ∈ 𝐶 ) } = ( { 𝑥 } × 𝐶 )
3	2	a1i	⊢ ( 𝑥 ∈ 𝐵 → { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 = 𝑥 ∧ 𝑏 ∈ 𝐶 ) } = ( { 𝑥 } × 𝐶 ) )
4	3	iuneq2i	⊢ ∪ 𝑥 ∈ 𝐵 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 = 𝑥 ∧ 𝑏 ∈ 𝐶 ) } = ∪ 𝑥 ∈ 𝐵 ( { 𝑥 } × 𝐶 )
5		iunxpconst	⊢ ∪ 𝑥 ∈ 𝐵 ( { 𝑥 } × 𝐶 ) = ( 𝐵 × 𝐶 )
6	4 5	eqtr2i	⊢ ( 𝐵 × 𝐶 ) = ∪ 𝑥 ∈ 𝐵 { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 = 𝑥 ∧ 𝑏 ∈ 𝐶 ) }