Theorem xrneq1

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

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

Proof

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