Theorem bj-evalval

Description: Value of the evaluation at a class. (Closed form of strfvnd and strfvn ). (Contributed by NM, 9-Sep-2011) (Revised by Mario Carneiro, 15-Nov-2014) (Revised by BJ, 27-Dec-2021)

	Ref	Expression
Assertion	bj-evalval	⊢ ( 𝐹 ∈ 𝑉 → ( Slot 𝐴 ‘ 𝐹 ) = ( 𝐹 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V )
2		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
3		df-slot	⊢ Slot 𝐴 = ( 𝑓 ∈ V ↦ ( 𝑓 ‘ 𝐴 ) )
4		fvex	⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
5	2 3 4	fvmpt	⊢ ( 𝐹 ∈ V → ( Slot 𝐴 ‘ 𝐹 ) = ( 𝐹 ‘ 𝐴 ) )
6	1 5	syl	⊢ ( 𝐹 ∈ 𝑉 → ( Slot 𝐴 ‘ 𝐹 ) = ( 𝐹 ‘ 𝐴 ) )