Theorem bj-diagval

Description: Value of the functionalized identity, or equivalently of the diagonal function. This expression views it as the functionalized identity, whereas bj-diagval2 views it as the diagonal function. See df-bj-diag for the terminology. (Contributed by BJ, 22-Jun-2019)

	Ref	Expression
Assertion	bj-diagval	$$⊢A\in V\to Id\left(A\right)={\mathrm{I}\upharpoonright }_A$$

Proof

Step	Hyp	Ref	Expression
1		df-bj-diag	$$⊢Id=\left(x\in \mathrm{V}⟼{\mathrm{I}\upharpoonright }_x\right)$$
2		reseq2	$$⊢x=A\to {\mathrm{I}\upharpoonright }_x={\mathrm{I}\upharpoonright }_A$$
3		elex	$$⊢A\in V\to A\in \mathrm{V}$$
4		resiexg	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A\in \mathrm{V}$$
5	1 2 3 4	fvmptd3	$$⊢A\in V\to Id\left(A\right)={\mathrm{I}\upharpoonright }_A$$