Database
BASIC STRUCTURES
Extensible structures
Basic definitions
basfn
Next ⟩
wunndx
Metamath Proof Explorer
Ascii
Structured
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