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

Metamath Proof Explorer

Theorem strndxid

Description: The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020) (New usage is discouraged.) Use strfvnd directly with N set to ( Endx ) if possible.

	Ref	Expression
Hypotheses	strndxid.s	$⊢ φ \to S \in V$
	strndxid.e	$⊢ E = Slot N$
	strndxid.n	$⊢ N \in ℕ$
Assertion	strndxid	$⊢ φ \to S (E (ndx)) = E (S)$

Proof

Step	Hyp	Ref	Expression
1		strndxid.s	$⊢ φ \to S \in V$
2		strndxid.e	$⊢ E = Slot N$
3		strndxid.n	$⊢ N \in ℕ$
4	2 3	ndxid	$⊢ E = Slot E (ndx)$
5	4 1	strfvnd	$⊢ φ \to E (S) = S (E (ndx))$
6	5	eqcomd	$⊢ φ \to S (E (ndx)) = E (S)$