Theorem slotfn

Description: A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypothesis	strfvnd.c	⊢ 𝐸 = Slot 𝑁
Assertion	slotfn	⊢ 𝐸 Fn V

Proof

Step	Hyp	Ref	Expression
1		strfvnd.c	⊢ 𝐸 = Slot 𝑁
2		fvex	⊢ ( 𝑥 ‘ 𝑁 ) ∈ V
3		df-slot	⊢ Slot 𝑁 = ( 𝑥 ∈ V ↦ ( 𝑥 ‘ 𝑁 ) )
4	1 3	eqtri	⊢ 𝐸 = ( 𝑥 ∈ V ↦ ( 𝑥 ‘ 𝑁 ) )
5	2 4	fnmpti	⊢ 𝐸 Fn V