Theorem basfn

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

	Ref	Expression
Assertion	basfn	|- Base Fn _V

Proof

Step	Hyp	Ref	Expression
1		baseid	|- Base = Slot ( Base ` ndx )
2	1	slotfn	|- Base Fn _V