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 X. C ) = U_ x e. B { <. a , b >. | ( a = x /\ b e. C ) }

Proof

Step	Hyp	Ref	Expression
1		xpsnopab	|- ( { x } X. C ) = { <. a , b >. | ( a = x /\ b e. C ) }
2	1	eqcomi	|- { <. a , b >. | ( a = x /\ b e. C ) } = ( { x } X. C )
3	2	a1i	|- ( x e. B -> { <. a , b >. | ( a = x /\ b e. C ) } = ( { x } X. C ) )
4	3	iuneq2i	|- U_ x e. B { <. a , b >. | ( a = x /\ b e. C ) } = U_ x e. B ( { x } X. C )
5		iunxpconst	|- U_ x e. B ( { x } X. C ) = ( B X. C )
6	4 5	eqtr2i	|- ( B X. C ) = U_ x e. B { <. a , b >. | ( a = x /\ b e. C ) }