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		df-base	|- Base = Slot 1
2	1	slotfn	|- Base Fn _V