Theorem bj-evalfn

Description: The evaluation at a class is a function on the universal class. (General form of slotfn ). (Contributed by Mario Carneiro, 22-Sep-2015) (Revised by BJ, 27-Dec-2021)

	Ref	Expression
Assertion	bj-evalfn	$$⊢\mathrm{Slot}AFn\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		fvex	$$⊢f\left(A\right)\in \mathrm{V}$$
2		df-slot	$$⊢\mathrm{Slot}A=\left(f\in \mathrm{V}⟼f\left(A\right)\right)$$
3	1 2	fnmpti	$$⊢\mathrm{Slot}AFn\mathrm{V}$$