Metamath Proof Explorer

Theorem xrneq12

Description: Equality theorem for the range Cartesian product. (Contributed by Peter Mazsa, 16-Dec-2020)

Ref Expression
Assertion xrneq12 
|- ( ( A = B /\ C = D ) -> ( A |X. C ) = ( B |X. D ) )

Proof

Step Hyp Ref Expression
1 xrneq1 
 |-  ( A = B -> ( A |X. C ) = ( B |X. C ) )
2 xrneq2 
 |-  ( C = D -> ( B |X. C ) = ( B |X. D ) )
3 1 2 sylan9eq 
 |-  ( ( A = B /\ C = D ) -> ( A |X. C ) = ( B |X. D ) )