Metamath Proof Explorer

Theorem xrneq1

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

Ref Expression
Assertion xrneq1 
|- ( A = B -> ( A |X. C ) = ( B |X. C ) )

Proof

Step Hyp Ref Expression
1 coeq2 
 |-  ( A = B -> ( `' ( 1st |` ( _V X. _V ) ) o. A ) = ( `' ( 1st |` ( _V X. _V ) ) o. B ) )
2 1 ineq1d 
 |-  ( A = B -> ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. C ) ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. B ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. C ) ) )
3 df-xrn 
 |-  ( A |X. C ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. C ) )
4 df-xrn 
 |-  ( B |X. C ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. B ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. C ) )
5 2 3 4 3eqtr4g 
 |-  ( A = B -> ( A |X. C ) = ( B |X. C ) )