Theorem xrneq12i

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

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

Proof

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