Theorem 1strbasOLD

Description: Obsolete proof of 1strbas as of 15-Nov-2024. The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	1str.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}$$
Assertion	1strbasOLD	$$⊢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	1strstr	$$⊢G\mathrm{Struct}⟨1,1⟩$$
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$$