Theorem bj-diagval2

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

	Ref	Expression
Assertion	bj-diagval2	|- ( A e. V -> ( _Id ` A ) = ( _I i^i ( A X. A ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-diagval	|- ( A e. V -> ( _Id ` A ) = ( _I |` A ) )
2		idinxpresid	|- ( _I i^i ( A X. A ) ) = ( _I |` A )
3	1 2	eqtr4di	|- ( A e. V -> ( _Id ` A ) = ( _I i^i ( A X. A ) ) )