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\in V\to \mathrm{Slot}A\left(F\right)=F\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢F\in V\to F\in \mathrm{V}$$
2		fveq1	$$⊢f=F\to f\left(A\right)=F\left(A\right)$$
3		df-slot	$$⊢\mathrm{Slot}A=\left(f\in \mathrm{V}⟼f\left(A\right)\right)$$
4		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
5	2 3 4	fvmpt	$$⊢F\in \mathrm{V}\to \mathrm{Slot}A\left(F\right)=F\left(A\right)$$
6	1 5	syl	$$⊢F\in V\to \mathrm{Slot}A\left(F\right)=F\left(A\right)$$