Metamath Proof Explorer


Theorem ixpconst

Description: Infinite Cartesian product of a constant B . (Contributed by NM, 28-Sep-2006)

Ref Expression
Hypotheses ixpconst.1 AV
ixpconst.2 BV
Assertion ixpconst xAB=BA

Proof

Step Hyp Ref Expression
1 ixpconst.1 AV
2 ixpconst.2 BV
3 ixpconstg AVBVxAB=BA
4 1 2 3 mp2an xAB=BA