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	$$⊢B\times C=\bigcup _{x\in B}\left\{⟨a,b⟩|\left(a=x\wedge b\in C\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		xpsnopab	$$⊢\left\{x\right\}\times C=\left\{⟨a,b⟩|\left(a=x\wedge b\in C\right)\right\}$$
2	1	eqcomi	$$⊢\left\{⟨a,b⟩|\left(a=x\wedge b\in C\right)\right\}=\left\{x\right\}\times C$$
3	2	a1i	$$⊢x\in B\to \left\{⟨a,b⟩|\left(a=x\wedge b\in C\right)\right\}=\left\{x\right\}\times C$$
4	3	iuneq2i	$$⊢\bigcup _{x\in B}\left\{⟨a,b⟩|\left(a=x\wedge b\in C\right)\right\}=\bigcup _{x\in B}\left(\left\{x\right\}\times C\right)$$
5		iunxpconst	$$⊢\bigcup _{x\in B}\left(\left\{x\right\}\times C\right)=B\times C$$
6	4 5	eqtr2i	$$⊢B\times C=\bigcup _{x\in B}\left\{⟨a,b⟩|\left(a=x\wedge b\in C\right)\right\}$$