This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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