Metamath Proof Explorer


Theorem ixpconstg

Description: Infinite Cartesian product of a constant B . (Contributed by Mario Carneiro, 11-Jan-2015)

Ref Expression
Assertion ixpconstg AVBWxAB=BA

Proof

Step Hyp Ref Expression
1 vex fV
2 1 elixpconst fxABf:AB
3 2 abbi2i xAB=f|f:AB
4 mapvalg BWAVBA=f|f:AB
5 3 4 eqtr4id BWAVxAB=BA
6 5 ancoms AVBWxAB=BA