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 = x B a b | a = x b C

Proof

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