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