Theorem 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$$

Proof

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