Database
BASIC STRUCTURES
Extensible structures
Basic definitions
base0
Next ⟩
strfvi
Metamath Proof Explorer
Ascii
Unicode
Theorem
base0
Description:
The base set of the empty structure.
(Contributed by
David A. Wheeler
, 7-Jul-2016)
Ref
Expression
Assertion
base0
⊢
∅
=
Base
∅
Proof
Step
Hyp
Ref
Expression
1
df-base
⊢
Base
=
Slot
1
2
1
str0
⊢
∅
=
Base
∅