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	⊢ ( 𝐴 ∈ 𝑉 → ( Id ‘ 𝐴 ) = ( I ∩ ( 𝐴 × 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-diagval	⊢ ( 𝐴 ∈ 𝑉 → ( Id ‘ 𝐴 ) = ( I ↾ 𝐴 ) )
2		idinxpresid	⊢ ( I ∩ ( 𝐴 × 𝐴 ) ) = ( I ↾ 𝐴 )
3	1 2	eqtr4di	⊢ ( 𝐴 ∈ 𝑉 → ( Id ‘ 𝐴 ) = ( I ∩ ( 𝐴 × 𝐴 ) ) )