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

Proof

Step	Hyp	Ref	Expression
1		bj-diagval	Could not format ( A e. V -> ( _Id ` A ) = ( _I |` A ) ) : No typesetting found for |- ( A e. V -> ( _Id ` A ) = ( _I |` A ) ) with typecode |-
2		idinxpresid	$$⊢\mathrm{I}\cap \left(A\times A\right)={\mathrm{I}\upharpoonright }_A$$
3	1 2	eqtr4di	Could not format ( A e. V -> ( _Id ` A ) = ( _I i^i ( A X. A ) ) ) : No typesetting found for |- ( A e. V -> ( _Id ` A ) = ( _I i^i ( A X. A ) ) ) with typecode |-