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	Could not format assertion : No typesetting found for |- ( A e. V -> ( _Id ` A ) = ( _I |` A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-bj-diag	Could not format _Id = ( x e. _V |-> ( _I |` x ) ) : No typesetting found for |- _Id = ( x e. _V |-> ( _I |` x ) ) with typecode |-
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	Could not format ( A e. V -> ( _Id ` A ) = ( _I |` A ) ) : No typesetting found for |- ( A e. V -> ( _Id ` A ) = ( _I |` A ) ) with typecode |-