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\in V\to Id\left(A\right)=\mathrm{I}\cap \left(A\times A\right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-diagval	$$⊢A\in V\to Id\left(A\right)={\mathrm{I}\upharpoonright }_A$$
2		idinxpresid	$$⊢\mathrm{I}\cap \left(A\times A\right)={\mathrm{I}\upharpoonright }_A$$
3	1 2	eqtr4di	$$⊢A\in V\to Id\left(A\right)=\mathrm{I}\cap \left(A\times A\right)$$