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=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}$$
Assertion	1strbas	$$⊢B\in V\to B={\mathrm{Base}}_G$$

Proof

Step	Hyp	Ref	Expression
1		1str.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}$$
2	1	1strstr1	$$⊢G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},{\mathrm{Base}}_{\mathrm{ndx}}⟩$$
3		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
4	1	eqimss2i	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}\subseteq G$$
5	2 3 4	strfv	$$⊢B\in V\to B={\mathrm{Base}}_G$$