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 A

Proof

Step	Hyp	Ref	Expression
1		df-slot	|- Slot A = ( f e. _V |-> ( f ` A ) )
2	1	funmpt2	|- Fun Slot A