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 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ }
Assertion 1strbas ( 𝐵𝑉𝐵 = ( Base ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 1str.g 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ }
2 1 1strstr1 𝐺 Struct ⟨ ( Base ‘ ndx ) , ( Base ‘ ndx ) ⟩
3 baseid Base = Slot ( Base ‘ ndx )
4 1 eqimss2i { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ } ⊆ 𝐺
5 2 3 4 strfv ( 𝐵𝑉𝐵 = ( Base ‘ 𝐺 ) )