Metamath Proof Explorer


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×C=xBab|a=xbC

Proof

Step Hyp Ref Expression
1 xpsnopab x×C=ab|a=xbC
2 1 eqcomi ab|a=xbC=x×C
3 2 a1i xBab|a=xbC=x×C
4 3 iuneq2i xBab|a=xbC=xBx×C
5 iunxpconst xBx×C=B×C
6 4 5 eqtr2i B×C=xBab|a=xbC