Theorem bj-evalfun

Description: The evaluation at a class is a function. (Contributed by BJ, 27-Dec-2021)

	Ref	Expression
Assertion	bj-evalfun	⊢ Fun Slot 𝐴

Proof

Step	Hyp	Ref	Expression
1		df-slot	⊢ Slot 𝐴 = ( 𝑓 ∈ V ↦ ( 𝑓 ‘ 𝐴 ) )
2	1	funmpt2	⊢ Fun Slot 𝐴