Metamath Proof Explorer

Theorem xpeq1i

Description: Equality inference for Cartesian product. (Contributed by NM, 21-Dec-2008)

Ref Expression
Hypothesis xpeq1i.1 
|- A = B
Assertion xpeq1i 
|- ( A X. C ) = ( B X. C )

Proof

Step Hyp Ref Expression
1 xpeq1i.1 
 |-  A = B
2 xpeq1 
 |-  ( A = B -> ( A X. C ) = ( B X. C ) )
3 1 2 ax-mp 
 |-  ( A X. C ) = ( B X. C )