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 ) )