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

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 baseid ⊢ Base = Slot ( Base ‘ ndx )
2 1 str0 ⊢ ∅ = ( Base ‘ ∅ )