Theorem bj-evalid

Description: The evaluation at a set of the identity function is that set. (General form of ndxarg .) The restriction to a set V is necessary since the argument of the function Slot A (like that of any function) has to be a set for the evaluation to be meaningful. (Contributed by BJ, 27-Dec-2021)

	Ref	Expression
Assertion	bj-evalid	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( Slot 𝐴 ‘ ( I ↾ 𝑉 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		resiexg	⊢ ( 𝑉 ∈ 𝑊 → ( I ↾ 𝑉 ) ∈ V )
2		bj-evalval	⊢ ( ( I ↾ 𝑉 ) ∈ V → ( Slot 𝐴 ‘ ( I ↾ 𝑉 ) ) = ( ( I ↾ 𝑉 ) ‘ 𝐴 ) )
3	1 2	syl	⊢ ( 𝑉 ∈ 𝑊 → ( Slot 𝐴 ‘ ( I ↾ 𝑉 ) ) = ( ( I ↾ 𝑉 ) ‘ 𝐴 ) )
4		fvresi	⊢ ( 𝐴 ∈ 𝑉 → ( ( I ↾ 𝑉 ) ‘ 𝐴 ) = 𝐴 )
5	3 4	sylan9eq	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( Slot 𝐴 ‘ ( I ↾ 𝑉 ) ) = 𝐴 )