Theorem bj-evalf

Description: The evaluation at a class is a function from the universal class into the universal class. (Contributed by BJ, 17-Mar-2026)

	Ref	Expression
Assertion	bj-evalf	⊢ Slot 𝐴 : V ⟶ V

Proof

Step	Hyp	Ref	Expression
1		df-slot	⊢ Slot 𝐴 = ( 𝑓 ∈ V ↦ ( 𝑓 ‘ 𝐴 ) )
2		fvexd	⊢ ( 𝑓 ∈ V → ( 𝑓 ‘ 𝐴 ) ∈ V )
3	1 2	fmpti	⊢ Slot 𝐴 : V ⟶ V