Metamath Proof Explorer


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