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 e. V -> ( _Id ` A ) = ( _I |` A ) )

Proof

Step	Hyp	Ref	Expression
1		df-bj-diag	|- _Id = ( x e. _V |-> ( _I |` x ) )
2		reseq2	|- ( x = A -> ( _I |` x ) = ( _I |` A ) )
3		elex	|- ( A e. V -> A e. _V )
4		resiexg	|- ( A e. V -> ( _I |` A ) e. _V )
5	1 2 3 4	fvmptd3	|- ( A e. V -> ( _Id ` A ) = ( _I |` A ) )