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	⊢ 𝐴 ∈ ( 1 ... 𝐵 )
Assertion	jm2.27dlem1	⊢ ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝐵 ) ) → ( 𝑎 ‘ 𝐴 ) = ( 𝑏 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		jm2.27dlem1.1	⊢ 𝐴 ∈ ( 1 ... 𝐵 )
2		fveq1	⊢ ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝐵 ) ) → ( 𝑎 ‘ 𝐴 ) = ( ( 𝑏 ↾ ( 1 ... 𝐵 ) ) ‘ 𝐴 ) )
3		fvres	⊢ ( 𝐴 ∈ ( 1 ... 𝐵 ) → ( ( 𝑏 ↾ ( 1 ... 𝐵 ) ) ‘ 𝐴 ) = ( 𝑏 ‘ 𝐴 ) )
4	1 3	ax-mp	⊢ ( ( 𝑏 ↾ ( 1 ... 𝐵 ) ) ‘ 𝐴 ) = ( 𝑏 ‘ 𝐴 )
5	2 4	eqtrdi	⊢ ( 𝑎 = ( 𝑏 ↾ ( 1 ... 𝐵 ) ) → ( 𝑎 ‘ 𝐴 ) = ( 𝑏 ‘ 𝐴 ) )