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 ` (/) )