Theorem reseq2i

Description: Equality inference for restrictions. (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Hypothesis	reseqi.1	|- A = B
Assertion	reseq2i	|- ( C |` A ) = ( C |` B )

Proof

Step	Hyp	Ref	Expression
1		reseqi.1	|- A = B
2		reseq2	|- ( A = B -> ( C |` A ) = ( C |` B ) )
3	1 2	ax-mp	|- ( C |` A ) = ( C |` B )