Metamath Proof Explorer


Theorem ixpint

Description: The intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015)

Ref Expression
Assertion ixpint BxAB=yBxAy

Proof

Step Hyp Ref Expression
1 ixpeq2 xAB=yByxAB=xAyBy
2 intiin B=yBy
3 2 a1i xAB=yBy
4 1 3 mprg xAB=xAyBy
5 ixpiin BxAyBy=yBxAy
6 4 5 eqtrid BxAB=yBxAy