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		df-base	$$⊢\mathrm{Base}=\mathrm{Slot}1$$
2	1	slotfn	$$⊢\mathrm{Base}Fn\mathrm{V}$$