Metamath Proof Explorer


Theorem 1strbas

Description: The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020)

Ref Expression
Hypothesis 1str.g
|- G = { <. ( Base ` ndx ) , B >. }
Assertion 1strbas
|- ( B e. V -> B = ( Base ` G ) )

Proof

Step Hyp Ref Expression
1 1str.g
 |-  G = { <. ( Base ` ndx ) , B >. }
2 1 1strstr
 |-  G Struct <. 1 , 1 >.
3 baseid
 |-  Base = Slot ( Base ` ndx )
4 1 eqimss2i
 |-  { <. ( Base ` ndx ) , B >. } C_ G
5 2 3 4 strfv
 |-  ( B e. V -> B = ( Base ` G ) )