Metamath Proof Explorer

Theorem 1strbas

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

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 1strstr1 
 |-  G Struct <. ( Base ` ndx ) , ( Base ` ndx ) >.
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 ) )