Theorem bj-evalid

Description: The evaluation at a set of the identity function is that set. (General form of ndxarg .) The restriction to a set V is necessary since the argument of the function Slot A (like that of any function) has to be a set for the evaluation to be meaningful. (Contributed by BJ, 27-Dec-2021)

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

Proof

Step	Hyp	Ref	Expression
1		resiexg	$$⊢V\in W\to {\mathrm{I}\upharpoonright }_V\in \mathrm{V}$$
2		bj-evalval	$$⊢{\mathrm{I}\upharpoonright }_V\in \mathrm{V}\to \mathrm{Slot}A\left({\mathrm{I}\upharpoonright }_V\right)=\left({\mathrm{I}\upharpoonright }_V\right)\left(A\right)$$
3	1 2	syl	$$⊢V\in W\to \mathrm{Slot}A\left({\mathrm{I}\upharpoonright }_V\right)=\left({\mathrm{I}\upharpoonright }_V\right)\left(A\right)$$
4		fvresi	$$⊢A\in V\to \left({\mathrm{I}\upharpoonright }_V\right)\left(A\right)=A$$
5	3 4	sylan9eq	$$⊢\left(V\in W\wedge A\in V\right)\to \mathrm{Slot}A\left({\mathrm{I}\upharpoonright }_V\right)=A$$