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	|- E = Slot N
Assertion	slotfn	|- E Fn _V

Proof

Step	Hyp	Ref	Expression
1		strfvnd.c	|- E = Slot N
2		fvex	|- ( x ` N ) e. _V
3		df-slot	|- Slot N = ( x e. _V |-> ( x ` N ) )
4	1 3	eqtri	|- E = ( x e. _V |-> ( x ` N ) )
5	2 4	fnmpti	|- E Fn _V