xrneq2

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

		Ref	Expression
	Assertion	xrneq2	$⊢ A = B \to C ⋉ A = C ⋉ B$

Step	Hyp	Ref	Expression
1		coeq2	$⊢ A = B \to {({2^{nd} ↾}_{(V \times V)})}^{-1} \circ A = {({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B$
2	1	ineq2d	$⊢ A = B \to ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ C) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ A) = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ C) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B)$
3		df-xrn	$⊢ C ⋉ A = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ C) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ A)$
4		df-xrn	$⊢ C ⋉ B = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ C) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B)$
5	2 3 4	3eqtr4g	$⊢ A = B \to C ⋉ A = C ⋉ B$

Metamath Proof Explorer