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=\mathrm{Slot}N$$
Assertion	slotfn	$$⊢EFn\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		strfvnd.c	$$⊢E=\mathrm{Slot}N$$
2		fvex	$$⊢x\left(N\right)\in \mathrm{V}$$
3		df-slot	$$⊢\mathrm{Slot}N=\left(x\in \mathrm{V}⟼x\left(N\right)\right)$$
4	1 3	eqtri	$$⊢E=\left(x\in \mathrm{V}⟼x\left(N\right)\right)$$
5	2 4	fnmpti	$$⊢EFn\mathrm{V}$$