Theorem jm2.27dlem1

Description: Lemma for rmydioph . Substitution of a tuple restriction into a projection that doesn't care. (Contributed by Stefan O'Rear, 11-Oct-2014)

	Ref	Expression
Hypothesis	jm2.27dlem1.1	|- A e. ( 1 ... B )
Assertion	jm2.27dlem1	|- ( a = ( b |` ( 1 ... B ) ) -> ( a ` A ) = ( b ` A ) )

Proof

Step	Hyp	Ref	Expression
1		jm2.27dlem1.1	|- A e. ( 1 ... B )
2		fveq1	|- ( a = ( b |` ( 1 ... B ) ) -> ( a ` A ) = ( ( b |` ( 1 ... B ) ) ` A ) )
3		fvres	|- ( A e. ( 1 ... B ) -> ( ( b |` ( 1 ... B ) ) ` A ) = ( b ` A ) )
4	1 3	ax-mp	|- ( ( b |` ( 1 ... B ) ) ` A ) = ( b ` A )
5	2 4	eqtrdi	|- ( a = ( b |` ( 1 ... B ) ) -> ( a ` A ) = ( b ` A ) )