Theorem reseq2

Description: Equality theorem for restrictions. (Contributed by NM, 8-Aug-1994)

	Ref	Expression
Assertion	reseq2	$$⊢A=B\to {C\upharpoonright }_A={C\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		xpeq1	$$⊢A=B\to A\times \mathrm{V}=B\times \mathrm{V}$$
2	1	ineq2d	$$⊢A=B\to C\cap \left(A\times \mathrm{V}\right)=C\cap \left(B\times \mathrm{V}\right)$$
3		df-res	$$⊢{C\upharpoonright }_A=C\cap \left(A\times \mathrm{V}\right)$$
4		df-res	$$⊢{C\upharpoonright }_B=C\cap \left(B\times \mathrm{V}\right)$$
5	2 3 4	3eqtr4g	$$⊢A=B\to {C\upharpoonright }_A={C\upharpoonright }_B$$