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\in \left(1\dots B\right)$$
Assertion	jm2.27dlem1	$$⊢a={b\upharpoonright }_{\left(1\dots B\right)}\to a\left(A\right)=b\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		jm2.27dlem1.1	$$⊢A\in \left(1\dots B\right)$$
2		fveq1	$$⊢a={b\upharpoonright }_{\left(1\dots B\right)}\to a\left(A\right)=\left({b\upharpoonright }_{\left(1\dots B\right)}\right)\left(A\right)$$
3		fvres	$$⊢A\in \left(1\dots B\right)\to \left({b\upharpoonright }_{\left(1\dots B\right)}\right)\left(A\right)=b\left(A\right)$$
4	1 3	ax-mp	$$⊢\left({b\upharpoonright }_{\left(1\dots B\right)}\right)\left(A\right)=b\left(A\right)$$
5	2 4	eqtrdi	$$⊢a={b\upharpoonright }_{\left(1\dots B\right)}\to a\left(A\right)=b\left(A\right)$$