This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in V \to B = {Base}_{G}$

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