Theorem reseq2

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

	Ref	Expression
Assertion	reseq2	|- ( A = B -> ( C |` A ) = ( C |` B ) )

Proof

Step	Hyp	Ref	Expression
1		xpeq1	|- ( A = B -> ( A X. _V ) = ( B X. _V ) )
2	1	ineq2d	|- ( A = B -> ( C i^i ( A X. _V ) ) = ( C i^i ( B X. _V ) ) )
3		df-res	|- ( C |` A ) = ( C i^i ( A X. _V ) )
4		df-res	|- ( C |` B ) = ( C i^i ( B X. _V ) )
5	2 3 4	3eqtr4g	|- ( A = B -> ( C |` A ) = ( C |` B ) )