Metamath Proof Explorer

Theorem xpeq12i

Description: Equality inference for Cartesian product. (Contributed by FL, 31-Aug-2009)

Ref Expression
Hypotheses xpeq12i.1 
|- A = B
xpeq12i.2 
|- C = D
Assertion xpeq12i 
|- ( A X. C ) = ( B X. D )

Proof

Step Hyp Ref Expression
1 xpeq12i.1 
 |-  A = B
2 xpeq12i.2 
 |-  C = D
3 xpeq12 
 |-  ( ( A = B /\ C = D ) -> ( A X. C ) = ( B X. D ) )
4 1 2 3 mp2an 
 |-  ( A X. C ) = ( B X. D )