Theorem bj-evalidval

Description: Closed general form of strndxid . Both sides are equal to ( FA ) by bj-evalid and bj-evalval respectively, but bj-evalidval adds something to bj-evalid and bj-evalval in that Slot A appears on both sides. (Contributed by BJ, 27-Dec-2021)

	Ref	Expression
Assertion	bj-evalidval	$$⊢\left(V\in W\wedge A\in V\wedge F\in U\right)\to F\left(\mathrm{Slot}A\left({\mathrm{I}\upharpoonright }_V\right)\right)=\mathrm{Slot}A\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-evalid	$$⊢\left(V\in W\wedge A\in V\right)\to \mathrm{Slot}A\left({\mathrm{I}\upharpoonright }_V\right)=A$$
2	1	fveq2d	$$⊢\left(V\in W\wedge A\in V\right)\to F\left(\mathrm{Slot}A\left({\mathrm{I}\upharpoonright }_V\right)\right)=F\left(A\right)$$
3	2	3adant3	$$⊢\left(V\in W\wedge A\in V\wedge F\in U\right)\to F\left(\mathrm{Slot}A\left({\mathrm{I}\upharpoonright }_V\right)\right)=F\left(A\right)$$
4		bj-evalval	$$⊢F\in U\to \mathrm{Slot}A\left(F\right)=F\left(A\right)$$
5	4	eqcomd	$$⊢F\in U\to F\left(A\right)=\mathrm{Slot}A\left(F\right)$$
6	5	3ad2ant3	$$⊢\left(V\in W\wedge A\in V\wedge F\in U\right)\to F\left(A\right)=\mathrm{Slot}A\left(F\right)$$
7	3 6	eqtrd	$$⊢\left(V\in W\wedge A\in V\wedge F\in U\right)\to F\left(\mathrm{Slot}A\left({\mathrm{I}\upharpoonright }_V\right)\right)=\mathrm{Slot}A\left(F\right)$$