Theorem xrneq2

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

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

Proof

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