Theorem basfn

Description: The base set extractor is a function on _V . (Contributed by Stefan O'Rear, 8-Jul-2015)

	Ref	Expression
Assertion	basfn	$$⊢\mathrm{Base}Fn\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
2	1	slotfn	$$⊢\mathrm{Base}Fn\mathrm{V}$$