Metamath Proof Explorer

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	⊢ Slot 𝐴 Fn V

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( 𝑓 ‘ 𝐴 ) ∈ V
2		df-slot	⊢ Slot 𝐴 = ( 𝑓 ∈ V ↦ ( 𝑓 ‘ 𝐴 ) )
3	1 2	fnmpti	⊢ Slot 𝐴 Fn V