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

Proof

Step	Hyp	Ref	Expression
1		df-bj-diag	⊢ Id = ( 𝑥 ∈ V ↦ ( I ↾ 𝑥 ) )
2		reseq2	⊢ ( 𝑥 = 𝐴 → ( I ↾ 𝑥 ) = ( I ↾ 𝐴 ) )
3		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
4		resiexg	⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) ∈ V )
5	1 2 3 4	fvmptd3	⊢ ( 𝐴 ∈ 𝑉 → ( Id ‘ 𝐴 ) = ( I ↾ 𝐴 ) )