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	|- ( F e. V -> ( Slot A ` F ) = ( F ` A ) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( F e. V -> F e. _V )
2		fveq1	|- ( f = F -> ( f ` A ) = ( F ` A ) )
3		df-slot	|- Slot A = ( f e. _V |-> ( f ` A ) )
4		fvex	|- ( F ` A ) e. _V
5	2 3 4	fvmpt	|- ( F e. _V -> ( Slot A ` F ) = ( F ` A ) )
6	1 5	syl	|- ( F e. V -> ( Slot A ` F ) = ( F ` A ) )